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  4623  tfr0dm  6380  tfr1onlemaccex  6406  tfrcllemaccex  6419  ertrd  6608  th3qlem1  6696  findcard2  6950  findcard2s  6951  diffifi  6955  fimax2gtrilemstep  6961  fidcenumlemrk  7020  fidcenumlemr  7021  isbth  7033  nninfninc  7189  cc2lem  7333  ltbtwnnqq  7482  prarloclemarch2  7486  addlocprlemeqgt  7599  addnqprlemrl  7624  addnqprlemru  7625  mulnqprlemrl  7640  mulnqprlemru  7641  ltexprlemrl  7677  ltexprlemru  7679  addcanprleml  7681  addcanprlemu  7682  recexprlemloc  7698  recexprlem1ssu  7701  cauappcvgprlemladdfl  7722  caucvgprlemloc  7742  caucvgprprlemloccalc  7751  letrd  8150  lelttrd  8151  lttrd  8152  ltletrd  8450  le2addd  8590  le2subd  8591  ltleaddd  8592  leltaddd  8593  lt2subd  8595  ltmul12a  8887  lediv12a  8921  lemul12ad  8969  lemul12bd  8970  lt2halvesd  9239  uzind  9437  uztrn  9618  xrlttrd  9884  xrlelttrd  9885  xrltletrd  9886  xrletrd  9887  ixxss1  9979  ixxss2  9980  ixxss12  9981  zsupcllemex  10320  zssinfcl  10322  fldiv4p1lem1div2  10395  seqf1og  10613  faclbnd3  10835  abs3lemd  11366  xrbdtri  11441  modfsummod  11623  mertenslemi1  11700  sin01gt0  11927  cos01gt0  11928  sin02gt0  11929  dvds2subd  11992  dvds2addd  11994  dvdstrd  11995  bezoutlemstep  12164  mulgcd  12183  gcddvdslcm  12241  lcmgcdeq  12251  mulgcddvds  12262  rpmulgcd2  12263  rpdvds  12267  divgcdcoprmex  12270  rpexp  12321  phimullem  12393  eulerthlem1  12395  eulerthlemrprm  12397  eulerthlemth  12400  prmdiveq  12404  pythagtriplem4  12437  pcqmul  12472  pcgcd1  12497  pcadd  12509  pockthlem  12525  4sqlem16  12575  exmidunben  12643  mulgass  13289  lmtopcnp  14486  blin2  14668  xmetxp  14743  tgqioo  14791  cncfmptid  14833  negcncf  14841  limcimolemlt  14900  plyadd  14987  plymul  14988  sinq12gt0  15066  logdivlti  15117  mpodvdsmulf1o  15226  perfectlem1  15235  2sqlem5  15360  2sqlem8  15364