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 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  pm2.26dc  912  orandc  945  19.9ht  1687  ax11v2  1866  ax11v  1873  ax11ev  1874  equs5or  1876  nfsbxy  1993  nfsbxyt  1994  nfabdw  2391  eqvisset  2811  vtoclgf  2860  vtoclg1f  2861  eueq3dc  2978  mo2icl  2983  csbiegf  3169  un00  3539  sneqr  3841  preqr1  3849  preq12b  3851  prel12  3852  nfopd  3877  ssex  4224  exmidundif  4294  iunpw  4575  nfimad  5083  dfrel2  5185  funsng  5373  cnvresid  5401  nffvd  5647  fnbrfvb  5680  funfvop  5755  acexmidlema  6004  tposf12  6430  supsnti  7198  pr2cv1  7394  exmidonfinlem  7397  sucpw1ne3  7443  sucpw1nel3  7444  recidnq  7606  ltaddnq  7620  ltadd1sr  7989  suplocsrlempr  8020  pncan3  8380  divcanap2  8853  ltp1  9017  ltm1  9019  recreclt  9073  nn0ind-raph  9590  2tnp1ge0ge0  10554  iswrdiz  11113  fsumcnv  11991  fprodcnv  12179  ef01bndlem  12310  sin01gt0  12316  cos01gt0  12317  ltoddhalfle  12447  bezoutlemnewy  12560  isprm5  12707  4sqlem12  12968  gsumval2  13473  nmznsg  13793  tangtx  15555  gausslemma2dlem1a  15780  lgseisenlem4  15795  2lgslem3a  15815  2lgslem3b  15816  2lgslem3c  15817  2lgslem3d  15818  bdsepnft  16432  bdssex  16447  bj-inex  16452  bj-d0clsepcl  16470  bj-2inf  16483  bj-inf2vnlem2  16516