Theorem mp2and 431

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 427	. 2 |- ( ph -> ( ch -> th ) )
5	1, 4	mpd 13	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  tfisi  4571  tfr0dm  6301  tfr1onlemaccex  6327  tfrcllemaccex  6340  ertrd  6529  th3qlem1  6615  findcard2  6867  findcard2s  6868  diffifi  6872  fimax2gtrilemstep  6878  fidcenumlemrk  6931  fidcenumlemr  6932  isbth  6944  cc2lem  7228  ltbtwnnqq  7377  prarloclemarch2  7381  addlocprlemeqgt  7494  addnqprlemrl  7519  addnqprlemru  7520  mulnqprlemrl  7535  mulnqprlemru  7536  ltexprlemrl  7572  ltexprlemru  7574  addcanprleml  7576  addcanprlemu  7577  recexprlemloc  7593  recexprlem1ssu  7596  cauappcvgprlemladdfl  7617  caucvgprlemloc  7637  caucvgprprlemloccalc  7646  letrd  8043  lelttrd  8044  lttrd  8045  ltletrd  8342  le2addd  8482  le2subd  8483  ltleaddd  8484  leltaddd  8485  lt2subd  8487  ltmul12a  8776  lediv12a  8810  lemul12ad  8858  lemul12bd  8859  lt2halvesd  9125  uzind  9323  uztrn  9503  xrlttrd  9766  xrlelttrd  9767  xrltletrd  9768  xrletrd  9769  ixxss1  9861  ixxss2  9862  ixxss12  9863  fldiv4p1lem1div2  10261  faclbnd3  10677  abs3lemd  11165  xrbdtri  11239  modfsummod  11421  mertenslemi1  11498  sin01gt0  11724  cos01gt0  11725  sin02gt0  11726  dvds2subd  11789  dvds2addd  11791  dvdstrd  11792  zsupcllemex  11901  zssinfcl  11903  bezoutlemstep  11952  mulgcd  11971  gcddvdslcm  12027  lcmgcdeq  12037  mulgcddvds  12048  rpmulgcd2  12049  rpdvds  12053  divgcdcoprmex  12056  rpexp  12107  phimullem  12179  eulerthlem1  12181  eulerthlemrprm  12183  eulerthlemth  12186  prmdiveq  12190  pythagtriplem4  12222  pcqmul  12257  pcgcd1  12281  pcadd  12293  pockthlem  12308  exmidunben  12381  lmtopcnp  13044  blin2  13226  xmetxp  13301  tgqioo  13341  cncfmptid  13377  negcncf  13382  limcimolemlt  13427  sinq12gt0  13545  logdivlti  13596  2sqlem5  13749  2sqlem8  13753