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  4683  tfr0dm  6483  tfr1onlemaccex  6509  tfrcllemaccex  6522  ertrd  6713  th3qlem1  6801  en2prd  6987  findcard2  7073  findcard2s  7074  diffifi  7078  fimax2gtrilemstep  7085  fidcenumlemrk  7147  fidcenumlemr  7148  isbth  7160  nninfninc  7316  cc2lem  7478  ltbtwnnqq  7628  prarloclemarch2  7632  addlocprlemeqgt  7745  addnqprlemrl  7770  addnqprlemru  7771  mulnqprlemrl  7786  mulnqprlemru  7787  ltexprlemrl  7823  ltexprlemru  7825  addcanprleml  7827  addcanprlemu  7828  recexprlemloc  7844  recexprlem1ssu  7847  cauappcvgprlemladdfl  7868  caucvgprlemloc  7888  caucvgprprlemloccalc  7897  letrd  8296  lelttrd  8297  lttrd  8298  ltletrd  8596  le2addd  8736  le2subd  8737  ltleaddd  8738  leltaddd  8739  lt2subd  8741  ltmul12a  9033  lediv12a  9067  lemul12ad  9115  lemul12bd  9116  lt2halvesd  9385  uzind  9584  uztrn  9766  xrlttrd  10037  xrlelttrd  10038  xrltletrd  10039  xrletrd  10040  ixxss1  10132  ixxss2  10133  ixxss12  10134  zsupcllemex  10483  zssinfcl  10485  fldiv4p1lem1div2  10558  seqf1og  10776  faclbnd3  10998  abs3lemd  11755  xrbdtri  11830  modfsummod  12012  mertenslemi1  12089  sin01gt0  12316  cos01gt0  12317  sin02gt0  12318  dvds2subd  12381  dvds2addd  12383  dvdstrd  12384  bezoutlemstep  12561  mulgcd  12580  gcddvdslcm  12638  lcmgcdeq  12648  mulgcddvds  12659  rpmulgcd2  12660  rpdvds  12664  divgcdcoprmex  12667  rpexp  12718  phimullem  12790  eulerthlem1  12792  eulerthlemrprm  12794  eulerthlemth  12797  prmdiveq  12801  pythagtriplem4  12834  pcqmul  12869  pcgcd1  12894  pcadd  12906  pockthlem  12922  4sqlem16  12972  exmidunben  13040  mulgass  13739  lmtopcnp  14967  blin2  15149  xmetxp  15224  tgqioo  15272  cncfmptid  15314  negcncf  15322  limcimolemlt  15381  plyadd  15468  plymul  15469  sinq12gt0  15547  logdivlti  15598  mpodvdsmulf1o  15707  perfectlem1  15716  2sqlem5  15841  2sqlem8  15845