Theorem mpbii 136

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 135	1 |- ( ph -> ch )

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

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

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  pm2.26dc  813  19.9ht  1532  ax11v2  1701  ax11v  1708  ax11ev  1709  equs5or  1711  nfsbxy  1818  nfsbxyt  1819  eqvisset  2565  vtoclgf  2612  eueq3dc  2715  mo2icl  2720  csbiegf  2890  un00  3263  sneqr  3531  preqr1  3539  preq12b  3541  prel12  3542  nfopd  3566  ssex  3894  iunpw  4211  nfimad  4677  dfrel2  4771  elxp5  4809  funsng  4946  cnvresid  4973  nffvd  5187  fnbrfvb  5214  funfvop  5279  acexmidlema  5503  tposf12  5884  recidnq  6491  ltaddnq  6505  ltadd1sr  6861  pncan3  7219  divcanap2  7659  ltp1  7810  ltm1  7812  recreclt  7866  nn0ind-raph  8355  2tnp1ge0ge0  9143  bdsepnft  10007  bdssex  10022  bj-inex  10027  bj-d0clsepcl  10049  bj-2inf  10062  bj-inf2vnlem2  10096