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  893  orandc  924  19.9ht  1621  ax11v2  1793  ax11v  1800  ax11ev  1801  equs5or  1803  nfsbxy  1916  nfsbxyt  1917  eqvisset  2699  vtoclgf  2747  vtoclg1f  2748  eueq3dc  2862  mo2icl  2867  csbiegf  3048  un00  3414  sneqr  3695  preqr1  3703  preq12b  3705  prel12  3706  nfopd  3730  ssex  4073  exmidundif  4137  iunpw  4409  nfimad  4898  dfrel2  4997  funsng  5177  cnvresid  5205  nffvd  5441  fnbrfvb  5470  funfvop  5540  acexmidlema  5773  tposf12  6174  supsnti  6900  exmidonfinlem  7066  recidnq  7225  ltaddnq  7239  ltadd1sr  7608  suplocsrlempr  7639  pncan3  7994  divcanap2  8464  ltp1  8626  ltm1  8628  recreclt  8682  nn0ind-raph  9192  2tnp1ge0ge0  10105  fsumcnv  11238  ef01bndlem  11499  sin01gt0  11504  cos01gt0  11505  ltoddhalfle  11626  bezoutlemnewy  11720  tangtx  12967  bdsepnft  13256  bdssex  13271  bj-inex  13276  bj-d0clsepcl  13294  bj-2inf  13307  bj-inf2vnlem2  13340