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  4563  tfr0dm  6286  tfr1onlemaccex  6312  tfrcllemaccex  6325  ertrd  6513  th3qlem1  6599  findcard2  6851  findcard2s  6852  diffifi  6856  fimax2gtrilemstep  6862  fidcenumlemrk  6915  fidcenumlemr  6916  isbth  6928  cc2lem  7203  ltbtwnnqq  7352  prarloclemarch2  7356  addlocprlemeqgt  7469  addnqprlemrl  7494  addnqprlemru  7495  mulnqprlemrl  7510  mulnqprlemru  7511  ltexprlemrl  7547  ltexprlemru  7549  addcanprleml  7551  addcanprlemu  7552  recexprlemloc  7568  recexprlem1ssu  7571  cauappcvgprlemladdfl  7592  caucvgprlemloc  7612  caucvgprprlemloccalc  7621  letrd  8018  lelttrd  8019  lttrd  8020  ltletrd  8317  le2addd  8457  le2subd  8458  ltleaddd  8459  leltaddd  8460  lt2subd  8462  ltmul12a  8751  lediv12a  8785  lemul12ad  8833  lemul12bd  8834  lt2halvesd  9100  uzind  9298  uztrn  9478  xrlttrd  9741  xrlelttrd  9742  xrltletrd  9743  xrletrd  9744  ixxss1  9836  ixxss2  9837  ixxss12  9838  fldiv4p1lem1div2  10236  faclbnd3  10652  abs3lemd  11139  xrbdtri  11213  modfsummod  11395  mertenslemi1  11472  sin01gt0  11698  cos01gt0  11699  sin02gt0  11700  dvds2subd  11763  dvds2addd  11765  dvdstrd  11766  zsupcllemex  11875  zssinfcl  11877  bezoutlemstep  11926  mulgcd  11945  gcddvdslcm  12001  lcmgcdeq  12011  mulgcddvds  12022  rpmulgcd2  12023  rpdvds  12027  divgcdcoprmex  12030  rpexp  12081  phimullem  12153  eulerthlem1  12155  eulerthlemrprm  12157  eulerthlemth  12160  prmdiveq  12164  pythagtriplem4  12196  pcqmul  12231  pcgcd1  12255  pcadd  12267  pockthlem  12282  exmidunben  12355  lmtopcnp  12850  blin2  13032  xmetxp  13107  tgqioo  13147  cncfmptid  13183  negcncf  13188  limcimolemlt  13233  sinq12gt0  13351  logdivlti  13402  2sqlem5  13555  2sqlem8  13559