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  1996  nfsbxyt  1997  nfabdw  2403  eqvisset  2823  vtoclgf  2872  vtoclg1f  2873  eueq3dc  2990  mo2icl  2995  csbiegf  3181  un00  3554  sneqr  3863  preqr1  3871  preq12b  3873  prel12  3874  nfopd  3899  ssex  4246  exmidundif  4318  iunpw  4600  nfimad  5109  dfrel2  5212  funsng  5401  cnvresid  5429  nffvd  5681  fnbrfvb  5714  funfvop  5789  acexmidlema  6040  tposf12  6499  supsnti  7295  pr2cv1  7491  exmidonfinlem  7495  sucpw1ne3  7541  sucpw1nel3  7542  recidnq  7704  ltaddnq  7718  ltadd1sr  8087  suplocsrlempr  8118  pncan3  8477  divcanap2  8950  ltp1  9114  ltm1  9116  recreclt  9170  nn0ind-raph  9691  2tnp1ge0ge0  10657  iswrdiz  11224  fsumcnv  12116  fprodcnv  12304  ef01bndlem  12435  sin01gt0  12441  cos01gt0  12442  ltoddhalfle  12572  bezoutlemnewy  12685  isprm5  12832  4sqlem12  13093  gsumval2  13599  nmznsg  13919  tangtx  15690  gausslemma2dlem1a  15918  lgseisenlem4  15933  2lgslem3a  15953  2lgslem3b  15954  2lgslem3c  15955  2lgslem3d  15956  bdsepnft  16644  bdssex  16659  bj-inex  16664  bj-d0clsepcl  16682  bj-2inf  16695  bj-inf2vnlem2  16728  gfsump1  16854