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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  pm2.26dc  919  orandc  952  19.9ht  1694  ax11v2  1873  ax11v  1880  ax11ev  1881  equs5or  1883  nfsbxy  2002  nfsbxyt  2003  nfabdw  2411  eqvisset  2832  vtoclgf  2881  vtoclg1f  2882  eueq3dc  3000  mo2icl  3005  csbiegf  3191  un00  3567  vvin  3569  sneqr  3885  preqr1  3893  preq12b  3895  prel12  3896  nfopd  3921  ssex  4270  exmidundif  4343  iunpw  4626  nfimad  5135  dfrel2  5238  funsng  5427  cnvresid  5455  nffvd  5707  fnbrfvb  5741  funfvop  5821  acexmidlema  6076  tposf12  6540  supsnti  7345  pr2cv1  7541  exmidonfinlem  7545  sucpw1ne3  7591  sucpw1nel3  7592  recidnq  7760  ltaddnq  7774  ltadd1sr  8143  suplocsrlempr  8174  pncan3  8534  divcanap2  9011  ltp1  9175  ltm1  9177  recreclt  9231  nn0ind-raph  9765  2tnp1ge0ge0  10738  iswrdiz  11313  fsumcnv  12206  fprodcnv  12394  ef01bndlem  12525  sin01gt0  12531  cos01gt0  12532  ltoddhalfle  12662  bezoutlemnewy  12775  isprm5  12922  4sqlem12  13183  gzsumval2  13716  nmznsg  14018  gsump1  14159  tangtx  15942  gausslemma2dlem1a  16189  lgseisenlem4  16204  2lgslem3a  16224  2lgslem3b  16225  2lgslem3c  16226  2lgslem3d  16227  bdsepnft  16925  bdssex  16940  bj-inex  16945  bj-d0clsepcl  16963  bj-2inf  16976  bj-inf2vnlem2  17009