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  2810  vtoclgf  2859  vtoclg1f  2860  eueq3dc  2977  mo2icl  2982  csbiegf  3168  un00  3538  sneqr  3838  preqr1  3846  preq12b  3848  prel12  3849  nfopd  3874  ssex  4221  exmidundif  4290  iunpw  4571  nfimad  5077  dfrel2  5179  funsng  5367  cnvresid  5395  nffvd  5639  fnbrfvb  5672  funfvop  5747  acexmidlema  5992  tposf12  6415  supsnti  7172  pr2cv1  7368  exmidonfinlem  7371  sucpw1ne3  7417  sucpw1nel3  7418  recidnq  7580  ltaddnq  7594  ltadd1sr  7963  suplocsrlempr  7994  pncan3  8354  divcanap2  8827  ltp1  8991  ltm1  8993  recreclt  9047  nn0ind-raph  9564  2tnp1ge0ge0  10521  iswrdiz  11078  fsumcnv  11948  fprodcnv  12136  ef01bndlem  12267  sin01gt0  12273  cos01gt0  12274  ltoddhalfle  12404  bezoutlemnewy  12517  isprm5  12664  4sqlem12  12925  gsumval2  13430  nmznsg  13750  tangtx  15512  gausslemma2dlem1a  15737  lgseisenlem4  15752  2lgslem3a  15772  2lgslem3b  15773  2lgslem3c  15774  2lgslem3d  15775  bdsepnft  16250  bdssex  16265  bj-inex  16270  bj-d0clsepcl  16288  bj-2inf  16301  bj-inf2vnlem2  16334