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  4685  tfr0dm  6488  tfr1onlemaccex  6514  tfrcllemaccex  6527  ertrd  6718  th3qlem1  6806  en2prd  6992  findcard2  7078  findcard2s  7079  diffifi  7083  fimax2gtrilemstep  7090  fidcenumlemrk  7153  fidcenumlemr  7154  isbth  7166  nninfninc  7322  cc2lem  7485  ltbtwnnqq  7635  prarloclemarch2  7639  addlocprlemeqgt  7752  addnqprlemrl  7777  addnqprlemru  7778  mulnqprlemrl  7793  mulnqprlemru  7794  ltexprlemrl  7830  ltexprlemru  7832  addcanprleml  7834  addcanprlemu  7835  recexprlemloc  7851  recexprlem1ssu  7854  cauappcvgprlemladdfl  7875  caucvgprlemloc  7895  caucvgprprlemloccalc  7904  letrd  8303  lelttrd  8304  lttrd  8305  ltletrd  8603  le2addd  8743  le2subd  8744  ltleaddd  8745  leltaddd  8746  lt2subd  8748  ltmul12a  9040  lediv12a  9074  lemul12ad  9122  lemul12bd  9123  lt2halvesd  9392  uzind  9591  uztrn  9773  xrlttrd  10044  xrlelttrd  10045  xrltletrd  10046  xrletrd  10047  ixxss1  10139  ixxss2  10140  ixxss12  10141  zsupcllemex  10491  zssinfcl  10493  fldiv4p1lem1div2  10566  seqf1og  10784  faclbnd3  11006  abs3lemd  11763  xrbdtri  11838  modfsummod  12021  mertenslemi1  12098  sin01gt0  12325  cos01gt0  12326  sin02gt0  12327  dvds2subd  12390  dvds2addd  12392  dvdstrd  12393  bezoutlemstep  12570  mulgcd  12589  gcddvdslcm  12647  lcmgcdeq  12657  mulgcddvds  12668  rpmulgcd2  12669  rpdvds  12673  divgcdcoprmex  12676  rpexp  12727  phimullem  12799  eulerthlem1  12801  eulerthlemrprm  12803  eulerthlemth  12806  prmdiveq  12810  pythagtriplem4  12843  pcqmul  12878  pcgcd1  12903  pcadd  12915  pockthlem  12931  4sqlem16  12981  exmidunben  13049  mulgass  13748  lmtopcnp  14977  blin2  15159  xmetxp  15234  tgqioo  15282  cncfmptid  15324  negcncf  15332  limcimolemlt  15391  plyadd  15478  plymul  15479  sinq12gt0  15557  logdivlti  15608  mpodvdsmulf1o  15717  perfectlem1  15726  2sqlem5  15851  2sqlem8  15855