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  908  orandc  941  19.9ht  1652  ax11v2  1831  ax11v  1838  ax11ev  1839  equs5or  1841  nfsbxy  1958  nfsbxyt  1959  nfabdw  2355  eqvisset  2770  vtoclgf  2819  vtoclg1f  2820  eueq3dc  2935  mo2icl  2940  csbiegf  3125  un00  3494  sneqr  3787  preqr1  3795  preq12b  3797  prel12  3798  nfopd  3822  ssex  4167  exmidundif  4236  iunpw  4512  nfimad  5015  dfrel2  5117  funsng  5301  cnvresid  5329  nffvd  5567  fnbrfvb  5598  funfvop  5671  acexmidlema  5910  tposf12  6324  supsnti  7066  exmidonfinlem  7255  sucpw1ne3  7294  sucpw1nel3  7295  recidnq  7455  ltaddnq  7469  ltadd1sr  7838  suplocsrlempr  7869  pncan3  8229  divcanap2  8701  ltp1  8865  ltm1  8867  recreclt  8921  nn0ind-raph  9437  2tnp1ge0ge0  10373  iswrdiz  10924  fsumcnv  11583  fprodcnv  11771  ef01bndlem  11902  sin01gt0  11908  cos01gt0  11909  ltoddhalfle  12037  bezoutlemnewy  12136  isprm5  12283  4sqlem12  12543  gsumval2  12983  nmznsg  13286  tangtx  15014  gausslemma2dlem1a  15215  lgseisenlem4  15230  2lgslem3a  15250  2lgslem3b  15251  2lgslem3c  15252  2lgslem3d  15253  bdsepnft  15449  bdssex  15464  bj-inex  15469  bj-d0clsepcl  15487  bj-2inf  15500  bj-inf2vnlem2  15533