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-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm2.26dc  875  orandc  906  19.9ht  1603  ax11v2  1774  ax11v  1781  ax11ev  1782  equs5or  1784  nfsbxy  1893  nfsbxyt  1894  eqvisset  2667  vtoclgf  2715  vtoclg1f  2716  eueq3dc  2827  mo2icl  2832  csbiegf  3009  un00  3375  sneqr  3653  preqr1  3661  preq12b  3663  prel12  3664  nfopd  3688  ssex  4025  exmidundif  4089  iunpw  4361  nfimad  4848  dfrel2  4947  funsng  5127  cnvresid  5155  nffvd  5387  fnbrfvb  5416  funfvop  5486  acexmidlema  5719  tposf12  6120  supsnti  6844  recidnq  7149  ltaddnq  7163  ltadd1sr  7519  pncan3  7893  divcanap2  8353  ltp1  8512  ltm1  8514  recreclt  8568  nn0ind-raph  9072  2tnp1ge0ge0  9967  fsumcnv  11098  ef01bndlem  11314  sin01gt0  11319  cos01gt0  11320  ltoddhalfle  11438  bezoutlemnewy  11530  bdsepnft  12777  bdssex  12792  bj-inex  12797  bj-d0clsepcl  12815  bj-2inf  12828  bj-inf2vnlem2  12861