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  909  orandc  942  19.9ht  1665  ax11v2  1844  ax11v  1851  ax11ev  1852  equs5or  1854  nfsbxy  1971  nfsbxyt  1972  nfabdw  2368  eqvisset  2783  vtoclgf  2832  vtoclg1f  2833  eueq3dc  2948  mo2icl  2953  csbiegf  3138  un00  3508  sneqr  3803  preqr1  3811  preq12b  3813  prel12  3814  nfopd  3838  ssex  4185  exmidundif  4254  iunpw  4531  nfimad  5036  dfrel2  5138  funsng  5325  cnvresid  5353  nffvd  5595  fnbrfvb  5626  funfvop  5699  acexmidlema  5942  tposf12  6362  supsnti  7114  exmidonfinlem  7308  sucpw1ne3  7351  sucpw1nel3  7352  recidnq  7513  ltaddnq  7527  ltadd1sr  7896  suplocsrlempr  7927  pncan3  8287  divcanap2  8760  ltp1  8924  ltm1  8926  recreclt  8980  nn0ind-raph  9497  2tnp1ge0ge0  10451  iswrdiz  11008  fsumcnv  11792  fprodcnv  11980  ef01bndlem  12111  sin01gt0  12117  cos01gt0  12118  ltoddhalfle  12248  bezoutlemnewy  12361  isprm5  12508  4sqlem12  12769  gsumval2  13273  nmznsg  13593  tangtx  15354  gausslemma2dlem1a  15579  lgseisenlem4  15594  2lgslem3a  15614  2lgslem3b  15615  2lgslem3c  15616  2lgslem3d  15617  bdsepnft  15897  bdssex  15912  bj-inex  15917  bj-d0clsepcl  15935  bj-2inf  15948  bj-inf2vnlem2  15981