Theorem mp2and 433

Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)

Hypotheses

Ref	Expression
mp2and.1	|- ( ph -> ps )
mp2and.2	|- ( ph -> ch )
mp2and.3	|- ( ph -> ( ( ps /\ ch ) -> th ) )

Assertion

Ref	Expression
mp2and	|- ( ph -> th )

Proof of Theorem mp2and

Step	Hyp	Ref	Expression
1		mp2and.2	. 2 |- ( ph -> ch )
2		mp2and.1	. . 3 |- ( ph -> ps )
3		mp2and.3	. . 3 |- ( ph -> ( ( ps /\ ch ) -> th ) )
4	2, 3	mpand 429	. 2 |- ( ph -> ( ch -> th ) )
5	1, 4	mpd 13	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  tfisi  4584  tfr0dm  6318  tfr1onlemaccex  6344  tfrcllemaccex  6357  ertrd  6546  th3qlem1  6632  findcard2  6884  findcard2s  6885  diffifi  6889  fimax2gtrilemstep  6895  fidcenumlemrk  6948  fidcenumlemr  6949  isbth  6961  cc2lem  7260  ltbtwnnqq  7409  prarloclemarch2  7413  addlocprlemeqgt  7526  addnqprlemrl  7551  addnqprlemru  7552  mulnqprlemrl  7567  mulnqprlemru  7568  ltexprlemrl  7604  ltexprlemru  7606  addcanprleml  7608  addcanprlemu  7609  recexprlemloc  7625  recexprlem1ssu  7628  cauappcvgprlemladdfl  7649  caucvgprlemloc  7669  caucvgprprlemloccalc  7678  letrd  8075  lelttrd  8076  lttrd  8077  ltletrd  8374  le2addd  8514  le2subd  8515  ltleaddd  8516  leltaddd  8517  lt2subd  8519  ltmul12a  8811  lediv12a  8845  lemul12ad  8893  lemul12bd  8894  lt2halvesd  9160  uzind  9358  uztrn  9538  xrlttrd  9803  xrlelttrd  9804  xrltletrd  9805  xrletrd  9806  ixxss1  9898  ixxss2  9899  ixxss12  9900  fldiv4p1lem1div2  10298  faclbnd3  10714  abs3lemd  11201  xrbdtri  11275  modfsummod  11457  mertenslemi1  11534  sin01gt0  11760  cos01gt0  11761  sin02gt0  11762  dvds2subd  11825  dvds2addd  11827  dvdstrd  11828  zsupcllemex  11937  zssinfcl  11939  bezoutlemstep  11988  mulgcd  12007  gcddvdslcm  12063  lcmgcdeq  12073  mulgcddvds  12084  rpmulgcd2  12085  rpdvds  12089  divgcdcoprmex  12092  rpexp  12143  phimullem  12215  eulerthlem1  12217  eulerthlemrprm  12219  eulerthlemth  12222  prmdiveq  12226  pythagtriplem4  12258  pcqmul  12293  pcgcd1  12317  pcadd  12329  pockthlem  12344  exmidunben  12417  mulgass  12947  lmtopcnp  13532  blin2  13714  xmetxp  13789  tgqioo  13829  cncfmptid  13865  negcncf  13870  limcimolemlt  13915  sinq12gt0  14033  logdivlti  14084  2sqlem5  14237  2sqlem8  14241