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-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  pm2.26dc  854  orandc  888  19.9ht  1584  ax11v2  1755  ax11v  1762  ax11ev  1763  equs5or  1765  nfsbxy  1873  nfsbxyt  1874  eqvisset  2643  vtoclgf  2691  vtoclg1f  2692  eueq3dc  2803  mo2icl  2808  csbiegf  2985  un00  3348  sneqr  3626  preqr1  3634  preq12b  3636  prel12  3637  nfopd  3661  ssex  3997  exmidundif  4058  iunpw  4330  nfimad  4816  dfrel2  4915  funsng  5094  cnvresid  5122  nffvd  5352  fnbrfvb  5380  funfvop  5450  acexmidlema  5681  tposf12  6072  supsnti  6780  recidnq  7049  ltaddnq  7063  ltadd1sr  7419  pncan3  7787  divcanap2  8244  ltp1  8402  ltm1  8404  recreclt  8458  nn0ind-raph  8962  2tnp1ge0ge0  9857  fsumcnv  10980  ef01bndlem  11196  sin01gt0  11201  cos01gt0  11202  ltoddhalfle  11320  bezoutlemnewy  11412  bdsepnft  12486  bdssex  12501  bj-inex  12506  bj-d0clsepcl  12528  bj-2inf  12541  bj-inf2vnlem2  12574