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  902  orandc  934  19.9ht  1634  ax11v2  1813  ax11v  1820  ax11ev  1821  equs5or  1823  nfsbxy  1935  nfsbxyt  1936  nfabdw  2331  eqvisset  2740  vtoclgf  2788  vtoclg1f  2789  eueq3dc  2904  mo2icl  2909  csbiegf  3092  un00  3461  sneqr  3747  preqr1  3755  preq12b  3757  prel12  3758  nfopd  3782  ssex  4126  exmidundif  4192  iunpw  4465  nfimad  4962  dfrel2  5061  funsng  5244  cnvresid  5272  nffvd  5508  fnbrfvb  5537  funfvop  5608  acexmidlema  5844  tposf12  6248  supsnti  6982  exmidonfinlem  7170  sucpw1ne3  7209  sucpw1nel3  7210  recidnq  7355  ltaddnq  7369  ltadd1sr  7738  suplocsrlempr  7769  pncan3  8127  divcanap2  8597  ltp1  8760  ltm1  8762  recreclt  8816  nn0ind-raph  9329  2tnp1ge0ge0  10257  fsumcnv  11400  fprodcnv  11588  ef01bndlem  11719  sin01gt0  11724  cos01gt0  11725  ltoddhalfle  11852  bezoutlemnewy  11951  isprm5  12096  tangtx  13553  bdsepnft  13922  bdssex  13937  bj-inex  13942  bj-d0clsepcl  13960  bj-2inf  13973  bj-inf2vnlem2  14006