Theorem mpbii 146

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

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  pm2.26dc  846  orandc  880  19.9ht  1572  ax11v2  1741  ax11v  1748  ax11ev  1749  equs5or  1751  nfsbxy  1859  nfsbxyt  1860  eqvisset  2609  vtoclgf  2657  eueq3dc  2766  mo2icl  2771  csbiegf  2946  un00  3290  sneqr  3552  preqr1  3560  preq12b  3562  prel12  3563  nfopd  3587  ssex  3915  iunpw  4229  nfimad  4697  dfrel2  4791  funsng  4966  cnvresid  4993  nffvd  5207  fnbrfvb  5235  funfvop  5300  acexmidlema  5523  tposf12  5907  supsnti  6418  recidnq  6583  ltaddnq  6597  ltadd1sr  6953  pncan3  7316  divcanap2  7768  ltp1  7922  ltm1  7924  recreclt  7978  nn0ind-raph  8464  2tnp1ge0ge0  9303  ltoddhalfle  10293  bezoutlemnewy  10385  bdsepnft  10678  bdssex  10693  bj-inex  10698  bj-d0clsepcl  10720  bj-2inf  10733  bj-inf2vnlem2  10766