MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mp2and Structured version   Unicode version

Theorem mp2and 679
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
StepHypRef Expression
1 mp2and.2 . 2  |-  ( ph  ->  ch )
2 mp2and.1 . . 3  |-  ( ph  ->  ps )
3 mp2and.3 . . 3  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
42, 3mpand 675 . 2  |-  ( ph  ->  ( ch  ->  th )
)
51, 4mpd 15 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  ssnelpssd  3746  tfisi  6472  tfindsg2  6475  smoord  6829  oelimcl  7042  oeeui  7044  nnawordex  7079  omabs  7089  ertrd  7120  th3qlem1  7209  omxpenlem  7415  ixpfi2  7612  supmax  7718  oismo  7757  cantnflem1c  7898  cantnflem1  7900  cantnflem3  7902  cantnflem1cOLD  7921  cantnflem1OLD  7923  cantnflem3OLD  7924  infxpenc2  8191  infxpenc2OLD  8195  axdc2lem  8620  r1limwun  8906  letrd  9531  lelttrd  9532  ltletrd  9534  lttrd  9535  le2addd  9960  le2subd  9961  ltleaddd  9962  leltaddd  9963  lt2subd  9965  ltmul12a  10188  lemul12ad  10278  lemul12bd  10279  lt2halvesd  10575  uzind  10736  uztrn  10880  xrlttrd  11136  xrlelttrd  11137  xrltletrd  11138  xrletrd  11139  supxrunb1  11285  supxrunb2  11286  ixxun  11319  ixxss1  11321  ixxss2  11322  ixxss12  11323  seqf1o  11850  faclbnd3  12071  sqrlem1  12735  sqrlem4  12738  sqrlem7  12741  abs3lemd  12950  rlimcn2  13071  o1of2  13093  lo1add  13107  lo1mul  13108  mertenslem1  13347  sin01gt0  13477  cos01gt0  13478  sin02gt0  13479  bitsmod  13635  sadaddlem  13665  bezoutlem4  13728  mulgcd  13733  mulgcddvds  13793  rpmulgcd2  13794  isprm5  13801  rpexp  13809  rpdvds  13813  phimullem  13857  eulerthlem1  13859  eulerthlem2  13860  prmdiv  13863  prmdiveq  13864  pythagtriplem4  13889  pcpremul  13913  pcqmul  13923  pcdvdstr  13945  pcgcd1  13946  pcadd  13954  pockthlem  13969  prmreclem2  13981  4sqlem8  14009  4sqlem10  14011  4sqlem14  14022  4sqlem16  14024  ramub1lem1  14090  ramub1lem2  14091  iscatd2  14622  joinval  15178  meetval  15192  lattrd  15231  latledi  15262  mulgass  15660  gaorber  15829  psgnunilem4  16006  efgredlem  16247  odadd2  16334  dmdprdpr  16551  ablfacrp2  16571  ablfac1b  16574  ablfac1eu  16577  pgpfac1  16584  gsumbagdiaglem  17448  znunit  17999  mdetunilem1  18421  mdetunilem4  18424  mdetunilem9  18429  neiptoptop  18738  lmcnp  18911  txcls  19180  txlly  19212  txnlly  19213  tx1stc  19226  alexsubALTlem1  19622  prdsmet  19948  blin2  20007  blcvx  20378  tgqioo  20380  metnrmlem3  20440  iscmet3lem2  20806  ovolmge0  20963  ovolunlem2  20984  mbfi1flimlem  21203  mbfmullem  21206  itg2add  21240  dvlip2  21470  dvge0  21481  dvcvx  21495  dvfsumabs  21498  plyadd  21688  plymul  21689  dgrlb  21707  plydivlem4  21765  vieta1lem2  21780  ulmdvlem3  21870  sinq12gt0  21972  logdivlti  22072  fsumharmonic  22408  fsumdvdsdiaglem  22526  dvdsmulf1o  22537  logfacubnd  22563  perfectlem1  22571  dchrptlem2  22607  lgsmod  22663  2sqlem3  22708  2sqlem5  22710  2sqlem8  22714  dchrisum0flblem2  22761  pntibndlem2  22843  pntlemr  22854  pntlemp  22862  axtgpasch  22931  axtgupdim2  22935  ex-natded5.2-2  23615  chscllem2  25044  chscllem4  25046  nmopge0  25318  nmfnge0  25334  nmoptrii  25501  staddi  25653  stadd3i  25655  atcvatlem  25792  supssd  26007  xrofsup  26058  xrge0addgt0  26157  archiabllem2c  26215  esumpmono  26531  erdszelem8  27089  txscon  27133  cvmlift2lem10  27204  cvmlift3lem7  27217  ghomgsg  27315  relexpsucl  27337  relexpcnv  27338  relexpdm  27340  relexprn  27341  rtrclreclem.trans  27351  dvdspw  27559  dfon2lem6  27604  dfon2lem8  27606  cgrtr4d  28019  cgrtrand  28027  cgrtr3and  28029  cgrextendand  28043  btwnexch3and  28055  btwnexchand  28060  linecgrand  28116  endofsegidand  28120  btwnconn1lem4  28124  btwnconn1lem8  28128  btwnconn1lem11  28131  btwnconn1lem12  28132  brsegle2  28143  seglecgr12im  28144  segleantisym  28149  colinbtwnle  28152  broutsideof2  28156  outsideoftr  28163  outsidele  28166  lineelsb2  28182  linethru  28187  heicant  28429  mbfresfi  28441  ftc1anclem6  28475  gtinf  28517  ismrcd2  29038  pellqrex  29223  jm2.17b  29307  dvdsacongtr  29330  jm2.26lem3  29353  jm2.27a  29357  jm2.27c  29359  fnwe2lem2  29407  addrcom  29734  stoweidlem15  29813  stoweidlem26  29824  stoweidlem28  29826  stoweidlem32  29830  stoweidlem44  29842  modfsummod  30248  wwlknredwwlkn  30361  wwlkextsur  30366  mpt2sn  30726  lcoss  30973  islindeps2  31020  isldepslvec2  31022  bnj1098  31780  bnj1110  31976  bnj1121  31979  riotasv2d  32611  lcvnbtwn2  32675  lcvnbtwn3  32676  lcvexchlem4  32685  omlfh1N  32906  atlen0  32958  atlatmstc  32967  cvratlem  33068  lnnat  33074  2atlt  33086  athgt  33103  1cvratex  33120  ps-2  33125  llncmp  33169  llncvrlpln  33205  lplncmp  33209  lplncvrlvol  33263  lvolcmp  33264  dalemcea  33307  dalem-cly  33318  dalem10  33320  dalem17  33327  dalem25  33345  dalem38  33357  dalem44  33363  dalem55  33374  2atm2atN  33432  cdlema1N  33438  paddasslem5  33471  dalawlem3  33520  dalawlem7  33524  dalawlem11  33528  dalawlem12  33529  lhp0lt  33650  4atexlemc  33716  cdlemg33a  34353  cdlemg33  34358  cdlemk51  34600  dia2dimlem2  34713  dia2dimlem3  34714  dihmeetlem20N  34974
  Copyright terms: Public domain W3C validator