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  919  orandc  952  19.9ht  1694  ax11v2  1873  ax11v  1880  ax11ev  1881  equs5or  1883  nfsbxy  2002  nfsbxyt  2003  nfabdw  2411  eqvisset  2832  vtoclgf  2881  vtoclg1f  2882  eueq3dc  3000  mo2icl  3005  csbiegf  3191  un00  3567  vvin  3569  sneqr  3883  preqr1  3891  preq12b  3893  prel12  3894  nfopd  3919  ssex  4268  exmidundif  4341  iunpw  4624  nfimad  5133  dfrel2  5236  funsng  5425  cnvresid  5453  nffvd  5705  fnbrfvb  5738  funfvop  5815  acexmidlema  6069  tposf12  6533  supsnti  7338  pr2cv1  7534  exmidonfinlem  7538  sucpw1ne3  7584  sucpw1nel3  7585  recidnq  7753  ltaddnq  7767  ltadd1sr  8136  suplocsrlempr  8167  pncan3  8527  divcanap2  9003  ltp1  9167  ltm1  9169  recreclt  9223  nn0ind-raph  9745  2tnp1ge0ge0  10717  iswrdiz  11292  fsumcnv  12185  fprodcnv  12373  ef01bndlem  12504  sin01gt0  12510  cos01gt0  12511  ltoddhalfle  12641  bezoutlemnewy  12754  isprm5  12901  4sqlem12  13162  gzsumval2  13694  nmznsg  13996  gsump1  14137  tangtx  15865  gausslemma2dlem1a  16094  lgseisenlem4  16109  2lgslem3a  16129  2lgslem3b  16130  2lgslem3c  16131  2lgslem3d  16132  bdsepnft  16830  bdssex  16845  bj-inex  16850  bj-d0clsepcl  16868  bj-2inf  16881  bj-inf2vnlem2  16914