Theorem mp2and 715

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

Syntax hints:   -> wi 4   /\ wa 384

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386

This theorem is referenced by:  reu2eqd  3403  ssnelpssd  3719  tfisi  7058  tfindsg2  7061  mpt2sn  7268  smoord  7462  oelimcl  7680  oeeui  7682  nnawordex  7717  omabs  7727  ertrd  7758  omxpenlem  8061  ixpfi2  8264  oismo  8445  cantnflem1c  8584  cantnflem1  8586  cantnflem3  8588  infxpenc2  8845  axdc2lem  9270  r1limwun  9558  letrd  10194  lelttrd  10195  ltletrd  10197  lttrd  10198  le2addd  10646  le2subd  10647  ltleaddd  10648  leltaddd  10649  lt2subd  10651  ltmul12a  10879  lemul12ad  10966  lemul12bd  10967  lt2halvesd  11280  uzind  11469  uztrn  11704  xrlttrd  11990  xrlelttrd  11991  xrltletrd  11992  xrletrd  11993  supxrunb1  12149  supxrunb2  12150  ixxun  12191  ixxss1  12193  ixxss2  12194  ixxss12  12195  fldiv4p1lem1div2  12636  fldiv4lem1div2uz2  12637  seqf1o  12842  faclbnd3  13079  rtrclreclem3  13800  sqrlem1  13983  sqrlem4  13986  sqrlem7  13989  abs3lemd  14200  rlimcn2  14321  o1of2  14343  lo1add  14357  lo1mul  14358  modfsummod  14526  mertenslem1  14616  sin01gt0  14920  cos01gt0  14921  sin02gt0  14922  dvds2subd  15017  bitsmod  15158  sadaddlem  15188  bezoutlem4  15259  mulgcd  15265  gcddvdslcm  15315  lcmgcdeq  15325  lcmfunsnlem2lem2  15352  mulgcddvds  15369  rpmulgcd2  15370  rpdvds  15374  divgcdcoprmex  15380  isprm5  15419  rpexp  15432  phimullem  15484  eulerthlem1  15486  eulerthlem2  15487  prmdiv  15490  prmdiveq  15491  pythagtriplem4  15524  pcpremul  15548  pcqmul  15558  pcdvdstr  15580  pcgcd1  15581  pcadd  15593  pockthlem  15609  prmreclem2  15621  4sqlem8  15649  4sqlem10  15651  4sqlem14  15662  4sqlem16  15664  ramub1lem1  15730  ramub1lem2  15731  prmdvdsprmop  15747  prmgaplem1  15753  prmgaplcmlem1  15755  prmgaplem7  15761  iscatd2  16342  cicsym  16464  initoeu2  16666  joinval  17005  meetval  17019  lattrd  17058  latledi  17089  mulgass  17579  gaorber  17741  psgnunilem4  17917  efgredlem  18160  odadd2  18252  dmdprdpr  18448  ablfacrp2  18466  ablfac1b  18469  ablfac1eu  18472  pgpfac1  18479  gsumbagdiaglem  19375  znunit  19912  mdetunilem1  20418  mdetunilem4  20421  mdetunilem9  20426  neiptoptop  20935  lmcnp  21108  txcls  21407  txlly  21439  txnlly  21440  tx1stc  21453  alexsubALTlem1  21851  prdsmet  22175  blin2  22234  blcvx  22601  tgqioo  22603  metnrmlem3  22664  iscmet3lem2  23090  ovolmge0  23245  ovolunlem2  23266  mbfi1flimlem  23489  mbfmullem  23492  itg2add  23526  dvlip2  23758  dvge0  23769  dvcvx  23783  dvfsumabs  23786  plyadd  23973  plymul  23974  dgrlb  23992  plydivlem4  24051  vieta1lem2  24066  ulmdvlem3  24156  sinq12gt0  24259  logdivlti  24366  fsumharmonic  24738  fsumdvdsdiaglem  24909  dvdsmulf1o  24920  logfacubnd  24946  perfectlem1  24954  dchrptlem2  24990  lgsmod  25048  2sqlem3  25145  2sqlem5  25147  2sqlem8  25151  dchrisum0flblem2  25198  pntibndlem2  25280  pntlemr  25291  pntlemp  25299  axtgpasch  25366  wlkcompim  26527  wwlksnredwwlkn  26790  wwlksnextsur  26795  upgr4cycl4dv4e  27045  ex-natded5.2-2  27262  chscllem2  28497  chscllem4  28499  nmopge0  28770  nmfnge0  28786  nmoptrii  28953  staddi  29105  stadd3i  29107  atcvatlem  29244  supssd  29487  infssd  29488  xrofsup  29533  2sqmod  29648  xrge0addgt0  29691  archiabllem2c  29749  orngmul  29803  esumpmono  30141  unelldsys  30221  omssubaddlem  30361  signstfvneq0  30649  axtgupdim2OLD  30746  bnj1098  30854  bnj1110  31050  bnj1121  31053  erdszelem8  31180  txsconn  31223  cvmlift2lem10  31294  cvmlift3lem7  31307  dvdspw  31636  sotrd  31655  dfon2lem6  31693  dfon2lem8  31695  nosupbnd1  31860  nosupbnd2lem1  31861  nosupbnd2  31862  noetalem3  31865  slttrd  31884  sltletrd  31885  slelttrd  31886  sletrd  31887  cgrtr4d  32092  cgrtrand  32100  cgrtr3and  32102  cgrextendand  32116  btwnexch3and  32128  btwnexchand  32133  linecgrand  32189  endofsegidand  32193  btwnconn1lem4  32197  btwnconn1lem8  32201  btwnconn1lem11  32204  btwnconn1lem12  32205  brsegle2  32216  seglecgr12im  32217  segleantisym  32222  colinbtwnle  32225  broutsideof2  32229  outsideoftr  32236  outsidele  32239  lineelsb2  32255  linethru  32260  gtinf  32313  gtinfOLD  32314  relowlssretop  33211  heicant  33444  mbfresfi  33456  ftc1anclem6  33490  riotasv2d  34243  lcvnbtwn2  34314  lcvnbtwn3  34315  lcvexchlem4  34324  omlfh1N  34545  atlen0  34597  atlatmstc  34606  cvratlem  34707  lnnat  34713  2atlt  34725  athgt  34742  1cvratex  34759  ps-2  34764  llncmp  34808  llncvrlpln  34844  lplncmp  34848  lplncvrlvol  34902  lvolcmp  34903  dalemcea  34946  dalem-cly  34957  dalem10  34959  dalem17  34966  dalem25  34984  dalem38  34996  dalem44  35002  dalem55  35013  2atm2atN  35071  cdlema1N  35077  paddasslem5  35110  dalawlem3  35159  dalawlem7  35163  dalawlem11  35167  dalawlem12  35168  lhp0lt  35289  4atexlemc  35355  cdlemg33a  35994  cdlemg33  35999  cdlemk51  36241  dia2dimlem2  36354  dia2dimlem3  36355  dihmeetlem20N  36615  ismrcd2  37262  pellqrex  37443  jm2.17b  37528  dvdsacongtr  37551  jm2.26lem3  37568  jm2.27a  37572  jm2.27c  37574  fnwe2lem2  37621  fco2d  38461  addrcom  38679  infxrunb2  39584  0ellimcdiv  39881  stoweidlem15  40232  stoweidlem26  40243  stoweidlem28  40245  stoweidlem32  40249  stoweidlem44  40261  icceuelpart  41372  perfectALTVlem1  41630  bgoldbtbndlem2  41694  bgoldbtbndlem3  41695  copisnmnd  41809  assintopass  41850  lcoss  42225  islindeps2  42272  isldepslvec2  42274  difmodm1lt  42317