Theorem mpbii 147

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

Syntax hints:   → wi 4   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm2.26dc  892  orandc  923  19.9ht  1620  ax11v2  1792  ax11v  1799  ax11ev  1800  equs5or  1802  nfsbxy  1915  nfsbxyt  1916  eqvisset  2696  vtoclgf  2744  vtoclg1f  2745  eueq3dc  2858  mo2icl  2863  csbiegf  3043  un00  3409  sneqr  3687  preqr1  3695  preq12b  3697  prel12  3698  nfopd  3722  ssex  4065  exmidundif  4129  iunpw  4401  nfimad  4890  dfrel2  4989  funsng  5169  cnvresid  5197  nffvd  5433  fnbrfvb  5462  funfvop  5532  acexmidlema  5765  tposf12  6166  supsnti  6892  exmidonfinlem  7049  recidnq  7201  ltaddnq  7215  ltadd1sr  7584  suplocsrlempr  7615  pncan3  7970  divcanap2  8440  ltp1  8602  ltm1  8604  recreclt  8658  nn0ind-raph  9168  2tnp1ge0ge0  10074  fsumcnv  11206  ef01bndlem  11463  sin01gt0  11468  cos01gt0  11469  ltoddhalfle  11590  bezoutlemnewy  11684  tangtx  12919  bdsepnft  13085  bdssex  13100  bj-inex  13105  bj-d0clsepcl  13123  bj-2inf  13136  bj-inf2vnlem2  13169