Theorem mpbii 148

Description: An inference from a nested biconditional, related to modus ponens. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-Oct-2012.)

Hypotheses

Ref	Expression
mpbii.min	⊢ 𝜓
mpbii.maj	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
mpbii	⊢ (𝜑 → 𝜒)

Proof of Theorem mpbii

Step	Hyp	Ref	Expression
1		mpbii.min	. . 3 ⊢ 𝜓
2	1	a1i 9	. 2 ⊢ (𝜑 → 𝜓)
3		mpbii.maj	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	2, 3	mpbid 147	1 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm2.26dc  919  orandc  952  19.9ht  1694  ax11v2  1873  ax11v  1880  ax11ev  1881  equs5or  1883  nfsbxy  2002  nfsbxyt  2003  nfabdw  2411  eqvisset  2832  vtoclgf  2881  vtoclg1f  2882  eueq3dc  3000  mo2icl  3005  csbiegf  3191  un00  3567  vvin  3569  sneqr  3885  preqr1  3893  preq12b  3895  prel12  3896  nfopd  3921  ssex  4272  exmidundif  4345  iunpw  4628  nfimad  5138  dfrel2  5241  funsng  5430  cnvresid  5458  nffvd  5710  fnbrfvb  5744  funfvop  5824  acexmidlema  6079  tposf12  6544  supsnti  7352  pr2cv1  7548  exmidonfinlem  7552  sucpw1ne3  7598  sucpw1nel3  7599  recidnq  7767  ltaddnq  7781  ltadd1sr  8150  suplocsrlempr  8181  pncan3  8542  divcanap2  9019  ltp1  9183  ltm1  9185  recreclt  9239  nn0ind-raph  9775  2tnp1ge0ge0  10758  iswrdiz  11334  fsumcnv  12230  fprodcnv  12418  ef01bndlem  12549  sin01gt0  12555  cos01gt0  12556  ltoddhalfle  12686  bezoutlemnewy  12799  isprm5  12947  4sqlem12  13211  gzsumval2  13774  nmznsg  14076  gsump1  14248  mvrf1fi  15215  tangtx  16077  gausslemma2dlem1a  16394  lgseisenlem4  16409  2lgslem3a  16429  2lgslem3b  16430  2lgslem3c  16431  2lgslem3d  16432  bdsepnft  17130  bdssex  17145  bj-inex  17150  bj-d0clsepcl  17168  bj-2inf  17181  bj-inf2vnlem2  17214