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  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  3883  preqr1  3891  preq12b  3893  prel12  3894  nfopd  3919  ssex  4268  exmidundif  4341  iunpw  4624  nfimad  5133  dfrel2  5236  funsng  5425  cnvresid  5453  nffvd  5705  fnbrfvb  5738  funfvop  5815  acexmidlema  6070  tposf12  6534  supsnti  7339  pr2cv1  7535  exmidonfinlem  7539  sucpw1ne3  7585  sucpw1nel3  7586  recidnq  7754  ltaddnq  7768  ltadd1sr  8137  suplocsrlempr  8168  pncan3  8528  divcanap2  9004  ltp1  9168  ltm1  9170  recreclt  9224  nn0ind-raph  9746  2tnp1ge0ge0  10719  iswrdiz  11294  fsumcnv  12187  fprodcnv  12375  ef01bndlem  12506  sin01gt0  12512  cos01gt0  12513  ltoddhalfle  12643  bezoutlemnewy  12756  isprm5  12903  4sqlem12  13164  gzsumval2  13697  nmznsg  13999  gsump1  14140  tangtx  15922  gausslemma2dlem1a  16160  lgseisenlem4  16175  2lgslem3a  16195  2lgslem3b  16196  2lgslem3c  16197  2lgslem3d  16198  bdsepnft  16896  bdssex  16911  bj-inex  16916  bj-d0clsepcl  16934  bj-2inf  16947  bj-inf2vnlem2  16980