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  2993  mo2icl  2998  csbiegf  3184  un00  3557  sneqr  3866  preqr1  3874  preq12b  3876  prel12  3877  nfopd  3902  ssex  4249  exmidundif  4321  iunpw  4603  nfimad  5112  dfrel2  5215  funsng  5404  cnvresid  5432  nffvd  5684  fnbrfvb  5717  funfvop  5792  acexmidlema  6043  tposf12  6502  supsnti  7298  pr2cv1  7494  exmidonfinlem  7498  sucpw1ne3  7544  sucpw1nel3  7545  recidnq  7713  ltaddnq  7727  ltadd1sr  8096  suplocsrlempr  8127  pncan3  8486  divcanap2  8959  ltp1  9123  ltm1  9125  recreclt  9179  nn0ind-raph  9701  2tnp1ge0ge0  10668  iswrdiz  11239  fsumcnv  12131  fprodcnv  12319  ef01bndlem  12450  sin01gt0  12456  cos01gt0  12457  ltoddhalfle  12587  bezoutlemnewy  12700  isprm5  12847  4sqlem12  13108  gsumval2  13631  nmznsg  13951  tangtx  15752  gausslemma2dlem1a  15980  lgseisenlem4  15995  2lgslem3a  16015  2lgslem3b  16016  2lgslem3c  16017  2lgslem3d  16018  bdsepnft  16706  bdssex  16721  bj-inex  16726  bj-d0clsepcl  16744  bj-2inf  16757  bj-inf2vnlem2  16790  gfsump1  16917