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  4588  tfr0dm  6325  tfr1onlemaccex  6351  tfrcllemaccex  6364  ertrd  6553  th3qlem1  6639  findcard2  6891  findcard2s  6892  diffifi  6896  fimax2gtrilemstep  6902  fidcenumlemrk  6955  fidcenumlemr  6956  isbth  6968  cc2lem  7267  ltbtwnnqq  7416  prarloclemarch2  7420  addlocprlemeqgt  7533  addnqprlemrl  7558  addnqprlemru  7559  mulnqprlemrl  7574  mulnqprlemru  7575  ltexprlemrl  7611  ltexprlemru  7613  addcanprleml  7615  addcanprlemu  7616  recexprlemloc  7632  recexprlem1ssu  7635  cauappcvgprlemladdfl  7656  caucvgprlemloc  7676  caucvgprprlemloccalc  7685  letrd  8083  lelttrd  8084  lttrd  8085  ltletrd  8382  le2addd  8522  le2subd  8523  ltleaddd  8524  leltaddd  8525  lt2subd  8527  ltmul12a  8819  lediv12a  8853  lemul12ad  8901  lemul12bd  8902  lt2halvesd  9168  uzind  9366  uztrn  9546  xrlttrd  9811  xrlelttrd  9812  xrltletrd  9813  xrletrd  9814  ixxss1  9906  ixxss2  9907  ixxss12  9908  fldiv4p1lem1div2  10307  faclbnd3  10725  abs3lemd  11212  xrbdtri  11286  modfsummod  11468  mertenslemi1  11545  sin01gt0  11771  cos01gt0  11772  sin02gt0  11773  dvds2subd  11836  dvds2addd  11838  dvdstrd  11839  zsupcllemex  11949  zssinfcl  11951  bezoutlemstep  12000  mulgcd  12019  gcddvdslcm  12075  lcmgcdeq  12085  mulgcddvds  12096  rpmulgcd2  12097  rpdvds  12101  divgcdcoprmex  12104  rpexp  12155  phimullem  12227  eulerthlem1  12229  eulerthlemrprm  12231  eulerthlemth  12234  prmdiveq  12238  pythagtriplem4  12270  pcqmul  12305  pcgcd1  12329  pcadd  12341  pockthlem  12356  exmidunben  12429  mulgass  13025  lmtopcnp  13789  blin2  13971  xmetxp  14046  tgqioo  14086  cncfmptid  14122  negcncf  14127  limcimolemlt  14172  sinq12gt0  14290  logdivlti  14341  2sqlem5  14505  2sqlem8  14509