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  915  orandc  948  19.9ht  1690  ax11v2  1869  ax11v  1876  ax11ev  1877  equs5or  1879  nfsbxy  1998  nfsbxyt  1999  nfabdw  2405  eqvisset  2826  vtoclgf  2875  vtoclg1f  2876  eueq3dc  2994  mo2icl  2999  csbiegf  3185  un00  3559  sneqr  3869  preqr1  3877  preq12b  3879  prel12  3880  nfopd  3905  ssex  4252  exmidundif  4324  iunpw  4606  nfimad  5115  dfrel2  5218  funsng  5407  cnvresid  5435  nffvd  5687  fnbrfvb  5720  funfvop  5795  acexmidlema  6049  tposf12  6513  supsnti  7309  pr2cv1  7505  exmidonfinlem  7509  sucpw1ne3  7555  sucpw1nel3  7556  recidnq  7724  ltaddnq  7738  ltadd1sr  8107  suplocsrlempr  8138  pncan3  8498  divcanap2  8974  ltp1  9138  ltm1  9140  recreclt  9194  nn0ind-raph  9716  2tnp1ge0ge0  10688  iswrdiz  11259  fsumcnv  12151  fprodcnv  12339  ef01bndlem  12470  sin01gt0  12476  cos01gt0  12477  ltoddhalfle  12607  bezoutlemnewy  12720  isprm5  12867  4sqlem12  13128  gsumval2  13663  nmznsg  13969  gfsump1  14111  tangtx  15832  gausslemma2dlem1a  16060  lgseisenlem4  16075  2lgslem3a  16095  2lgslem3b  16096  2lgslem3c  16097  2lgslem3d  16098  bdsepnft  16796  bdssex  16811  bj-inex  16816  bj-d0clsepcl  16834  bj-2inf  16847  bj-inf2vnlem2  16880