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  914  orandc  947  19.9ht  1689  ax11v2  1868  ax11v  1875  ax11ev  1876  equs5or  1878  nfsbxy  1995  nfsbxyt  1996  nfabdw  2393  eqvisset  2813  vtoclgf  2862  vtoclg1f  2863  eueq3dc  2980  mo2icl  2985  csbiegf  3171  un00  3541  sneqr  3843  preqr1  3851  preq12b  3853  prel12  3854  nfopd  3879  ssex  4226  exmidundif  4296  iunpw  4577  nfimad  5085  dfrel2  5187  funsng  5376  cnvresid  5404  nffvd  5651  fnbrfvb  5684  funfvop  5759  acexmidlema  6009  tposf12  6435  supsnti  7204  pr2cv1  7400  exmidonfinlem  7404  sucpw1ne3  7450  sucpw1nel3  7451  recidnq  7613  ltaddnq  7627  ltadd1sr  7996  suplocsrlempr  8027  pncan3  8387  divcanap2  8860  ltp1  9024  ltm1  9026  recreclt  9080  nn0ind-raph  9597  2tnp1ge0ge0  10562  iswrdiz  11121  fsumcnv  12000  fprodcnv  12188  ef01bndlem  12319  sin01gt0  12325  cos01gt0  12326  ltoddhalfle  12456  bezoutlemnewy  12569  isprm5  12716  4sqlem12  12977  gsumval2  13482  nmznsg  13802  tangtx  15565  gausslemma2dlem1a  15790  lgseisenlem4  15805  2lgslem3a  15825  2lgslem3b  15826  2lgslem3c  15827  2lgslem3d  15828  bdsepnft  16503  bdssex  16518  bj-inex  16523  bj-d0clsepcl  16541  bj-2inf  16554  bj-inf2vnlem2  16587  gfsump1  16707