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  2818  vtoclg1f  2819  eueq3dc  2934  mo2icl  2939  csbiegf  3124  un00  3493  sneqr  3786  preqr1  3794  preq12b  3796  prel12  3797  nfopd  3821  ssex  4166  exmidundif  4235  iunpw  4511  nfimad  5014  dfrel2  5116  funsng  5300  cnvresid  5328  nffvd  5566  fnbrfvb  5597  funfvop  5670  acexmidlema  5909  tposf12  6322  supsnti  7064  exmidonfinlem  7253  sucpw1ne3  7292  sucpw1nel3  7293  recidnq  7453  ltaddnq  7467  ltadd1sr  7836  suplocsrlempr  7867  pncan3  8227  divcanap2  8699  ltp1  8863  ltm1  8865  recreclt  8919  nn0ind-raph  9434  2tnp1ge0ge0  10370  iswrdiz  10921  fsumcnv  11580  fprodcnv  11768  ef01bndlem  11899  sin01gt0  11905  cos01gt0  11906  ltoddhalfle  12034  bezoutlemnewy  12133  isprm5  12280  4sqlem12  12540  gsumval2  12980  nmznsg  13283  tangtx  14973  gausslemma2dlem1a  15174  lgseisenlem4  15189  bdsepnft  15379  bdssex  15394  bj-inex  15399  bj-d0clsepcl  15417  bj-2inf  15430  bj-inf2vnlem2  15463