Theorem mp2and 430

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 426	. 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  4540  tfr0dm  6259  tfr1onlemaccex  6285  tfrcllemaccex  6298  ertrd  6485  th3qlem1  6571  findcard2  6823  findcard2s  6824  diffifi  6828  fimax2gtrilemstep  6834  fidcenumlemrk  6887  fidcenumlemr  6888  isbth  6900  cc2lem  7165  ltbtwnnqq  7314  prarloclemarch2  7318  addlocprlemeqgt  7431  addnqprlemrl  7456  addnqprlemru  7457  mulnqprlemrl  7472  mulnqprlemru  7473  ltexprlemrl  7509  ltexprlemru  7511  addcanprleml  7513  addcanprlemu  7514  recexprlemloc  7530  recexprlem1ssu  7533  cauappcvgprlemladdfl  7554  caucvgprlemloc  7574  caucvgprprlemloccalc  7583  letrd  7978  lelttrd  7979  lttrd  7980  ltletrd  8277  le2addd  8417  le2subd  8418  ltleaddd  8419  leltaddd  8420  lt2subd  8422  ltmul12a  8710  lediv12a  8744  lemul12ad  8792  lemul12bd  8793  lt2halvesd  9059  uzind  9254  uztrn  9434  xrlttrd  9691  xrlelttrd  9692  xrltletrd  9693  xrletrd  9694  ixxss1  9786  ixxss2  9787  ixxss12  9788  fldiv4p1lem1div2  10182  faclbnd3  10594  abs3lemd  11078  xrbdtri  11150  modfsummod  11332  mertenslemi1  11409  sin01gt0  11635  cos01gt0  11636  sin02gt0  11637  dvds2subd  11696  zsupcllemex  11806  zssinfcl  11808  bezoutlemstep  11853  mulgcd  11872  gcddvdslcm  11922  lcmgcdeq  11932  mulgcddvds  11943  rpmulgcd2  11944  rpdvds  11948  divgcdcoprmex  11951  rpexp  11999  phimullem  12069  eulerthlem1  12071  eulerthlemrprm  12073  eulerthlemth  12076  exmidunben  12114  lmtopcnp  12597  blin2  12779  xmetxp  12854  tgqioo  12894  cncfmptid  12930  negcncf  12935  limcimolemlt  12980  sinq12gt0  13098  logdivlti  13149