Theorem mpbii 146

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

Syntax hints:   → wi 4   ↔ wb 103

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm2.26dc  847  orandc  881  19.9ht  1573  ax11v2  1743  ax11v  1750  ax11ev  1751  equs5or  1753  nfsbxy  1861  nfsbxyt  1862  eqvisset  2619  vtoclgf  2667  eueq3dc  2776  mo2icl  2781  csbiegf  2956  un00  3307  sneqr  3573  preqr1  3581  preq12b  3583  prel12  3584  nfopd  3608  ssex  3936  exmidundif  3992  iunpw  4258  nfimad  4728  dfrel2  4822  funsng  4997  cnvresid  5025  nffvd  5240  fnbrfvb  5268  funfvop  5333  acexmidlema  5556  tposf12  5940  supsnti  6514  recidnq  6722  ltaddnq  6736  ltadd1sr  7092  pncan3  7460  divcanap2  7912  ltp1  8066  ltm1  8068  recreclt  8122  nn0ind-raph  8622  2tnp1ge0ge0  9460  ltoddhalfle  10525  bezoutlemnewy  10617  bdsepnft  10970  bdssex  10985  bj-inex  10990  bj-d0clsepcl  11012  bj-2inf  11025  bj-inf2vnlem2  11058