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  914  orandc  947  19.9ht  1689  ax11v2  1867  ax11v  1874  ax11ev  1875  equs5or  1877  nfsbxy  1994  nfsbxyt  1995  nfabdw  2392  eqvisset  2812  vtoclgf  2861  vtoclg1f  2862  eueq3dc  2979  mo2icl  2984  csbiegf  3170  un00  3540  sneqr  3844  preqr1  3852  preq12b  3854  prel12  3855  nfopd  3880  ssex  4227  exmidundif  4298  iunpw  4579  nfimad  5087  dfrel2  5189  funsng  5378  cnvresid  5406  nffvd  5654  fnbrfvb  5687  funfvop  5762  acexmidlema  6014  tposf12  6440  supsnti  7209  pr2cv1  7405  exmidonfinlem  7409  sucpw1ne3  7455  sucpw1nel3  7456  recidnq  7618  ltaddnq  7632  ltadd1sr  8001  suplocsrlempr  8032  pncan3  8392  divcanap2  8865  ltp1  9029  ltm1  9031  recreclt  9085  nn0ind-raph  9602  2tnp1ge0ge0  10567  iswrdiz  11129  fsumcnv  12021  fprodcnv  12209  ef01bndlem  12340  sin01gt0  12346  cos01gt0  12347  ltoddhalfle  12477  bezoutlemnewy  12590  isprm5  12737  4sqlem12  12998  gsumval2  13503  nmznsg  13823  tangtx  15591  gausslemma2dlem1a  15816  lgseisenlem4  15831  2lgslem3a  15851  2lgslem3b  15852  2lgslem3c  15853  2lgslem3d  15854  bdsepnft  16542  bdssex  16557  bj-inex  16562  bj-d0clsepcl  16580  bj-2inf  16593  bj-inf2vnlem2  16626  gfsump1  16754