Theorem mpbii 147

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	|- ps
mpbii.maj	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
mpbii	|- ( ph -> ch )

Proof of Theorem mpbii

Step	Hyp	Ref	Expression
1		mpbii.min	. . 3 |- ps
2	1	a1i 9	. 2 |- ( ph -> ps )
3		mpbii.maj	. 2 |- ( ph -> ( ps <-> ch ) )
4	2, 3	mpbid 146	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm2.26dc  897  orandc  929  19.9ht  1629  ax11v2  1808  ax11v  1815  ax11ev  1816  equs5or  1818  nfsbxy  1930  nfsbxyt  1931  nfabdw  2327  eqvisset  2736  vtoclgf  2784  vtoclg1f  2785  eueq3dc  2900  mo2icl  2905  csbiegf  3088  un00  3455  sneqr  3740  preqr1  3748  preq12b  3750  prel12  3751  nfopd  3775  ssex  4119  exmidundif  4185  iunpw  4458  nfimad  4955  dfrel2  5054  funsng  5234  cnvresid  5262  nffvd  5498  fnbrfvb  5527  funfvop  5597  acexmidlema  5833  tposf12  6237  supsnti  6970  exmidonfinlem  7149  sucpw1ne3  7188  sucpw1nel3  7189  recidnq  7334  ltaddnq  7348  ltadd1sr  7717  suplocsrlempr  7748  pncan3  8106  divcanap2  8576  ltp1  8739  ltm1  8741  recreclt  8795  nn0ind-raph  9308  2tnp1ge0ge0  10236  fsumcnv  11378  fprodcnv  11566  ef01bndlem  11697  sin01gt0  11702  cos01gt0  11703  ltoddhalfle  11830  bezoutlemnewy  11929  isprm5  12074  tangtx  13399  bdsepnft  13769  bdssex  13784  bj-inex  13789  bj-d0clsepcl  13807  bj-2inf  13820  bj-inf2vnlem2  13853