Theorem mp2and 437

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  tfisi  4736  tfr0dm  6598  tfr1onlemaccex  6624  tfrcllemaccex  6637  ertrd  6828  th3qlem1  6916  en2prd  7112  findcard2  7199  findcard2s  7200  diffifi  7204  fimax2gtrilemstep  7211  fidcenumlemrk  7278  fidcenumlemr  7279  isbth  7291  nninfninc  7470  cc2lem  7639  ltbtwnnqq  7789  prarloclemarch2  7793  addlocprlemeqgt  7906  addnqprlemrl  7931  addnqprlemru  7932  mulnqprlemrl  7947  mulnqprlemru  7948  ltexprlemrl  7984  ltexprlemru  7986  addcanprleml  7988  addcanprlemu  7989  recexprlemloc  8005  recexprlem1ssu  8008  cauappcvgprlemladdfl  8029  caucvgprlemloc  8049  caucvgprprlemloccalc  8058  letrd  8458  lelttrd  8459  lttrd  8460  ltletrd  8759  le2addd  8900  le2subd  8901  ltleaddd  8902  leltaddd  8903  lt2subd  8905  ltmul12a  9199  lediv12a  9233  lemul12ad  9281  lemul12bd  9282  lt2halvesd  9565  uzind  9768  uztrn  9955  xrlttrd  10228  xrlelttrd  10229  xrltletrd  10230  xrletrd  10231  ixxss1  10323  ixxss2  10324  ixxss12  10325  zsupcllemex  10680  zssinfcl  10682  fldiv4p1lem1div2  10761  seqf1og  10979  faclbnd3  11203  abs3lemd  11990  xrbdtri  12067  modfsummod  12250  mertenslemi1  12327  sin01gt0  12554  cos01gt0  12555  sin02gt0  12556  dvds2subd  12619  dvds2addd  12621  dvdstrd  12622  bezoutlemstep  12799  mulgcd  12818  gcddvdslcm  12876  lcmgcdeq  12886  mulgcddvds  12897  rpmulgcd2  12898  rpdvds  12902  divgcdcoprmex  12905  rpexp  12957  phimullem  13032  eulerthlem1  13034  eulerthlemrprm  13036  eulerthlemth  13039  prmdiveq  13043  pythagtriplem4  13076  pcqmul  13111  pcgcd1  13136  pcadd  13148  pockthlem  13164  4sqlem16  13214  exmidunben  13375  mulgass  14021  gsumbagdiaglem  15194  lmtopcnp  15509  blin2  15691  xmetxp  15766  tgqioo  15814  cncfmptid  15856  negcncf  15864  limcimolemlt  15923  plyadd  16010  plymul  16011  sinq12gt0  16090  logdivlti  16144  ppiprm  16292  mpodvdsmulf1o  16317  perfectlem1  16332  2sqlem5  16476  2sqlem8  16480