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  911  orandc  944  19.9ht  1667  ax11v2  1846  ax11v  1853  ax11ev  1854  equs5or  1856  nfsbxy  1973  nfsbxyt  1974  nfabdw  2371  eqvisset  2790  vtoclgf  2839  vtoclg1f  2840  eueq3dc  2957  mo2icl  2962  csbiegf  3148  un00  3518  sneqr  3817  preqr1  3825  preq12b  3827  prel12  3828  nfopd  3853  ssex  4200  exmidundif  4269  iunpw  4548  nfimad  5053  dfrel2  5155  funsng  5343  cnvresid  5371  nffvd  5615  fnbrfvb  5646  funfvop  5720  acexmidlema  5965  tposf12  6385  supsnti  7140  pr2cv1  7336  exmidonfinlem  7339  sucpw1ne3  7385  sucpw1nel3  7386  recidnq  7548  ltaddnq  7562  ltadd1sr  7931  suplocsrlempr  7962  pncan3  8322  divcanap2  8795  ltp1  8959  ltm1  8961  recreclt  9015  nn0ind-raph  9532  2tnp1ge0ge0  10488  iswrdiz  11045  fsumcnv  11914  fprodcnv  12102  ef01bndlem  12233  sin01gt0  12239  cos01gt0  12240  ltoddhalfle  12370  bezoutlemnewy  12483  isprm5  12630  4sqlem12  12891  gsumval2  13396  nmznsg  13716  tangtx  15477  gausslemma2dlem1a  15702  lgseisenlem4  15717  2lgslem3a  15737  2lgslem3b  15738  2lgslem3c  15739  2lgslem3d  15740  bdsepnft  16160  bdssex  16175  bj-inex  16180  bj-d0clsepcl  16198  bj-2inf  16211  bj-inf2vnlem2  16244