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

Theorem mp2and 683
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 679 . 2  |-  ( ph  ->  ( ch  ->  th )
)
51, 4mpd 15 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  reu2eqd  3267  ssnelpssd  3860  tfisi  6699  tfindsg2  6702  mpt2sn  6898  smoord  7095  oelimcl  7312  oeeui  7314  nnawordex  7349  omabs  7359  ertrd  7390  omxpenlem  7682  ixpfi2  7881  supmaxOLD  7992  oismo  8064  cantnflem1c  8200  cantnflem1  8202  cantnflem3  8204  infxpenc2  8460  axdc2lem  8885  r1limwun  9168  letrd  9799  lelttrd  9800  ltletrd  9802  lttrd  9803  le2addd  10239  le2subd  10240  ltleaddd  10241  leltaddd  10242  lt2subd  10244  ltmul12a  10468  lemul12ad  10556  lemul12bd  10557  lt2halvesd  10867  uzind  11034  uztrn  11182  xrlttrd  11463  xrlelttrd  11464  xrltletrd  11465  xrletrd  11466  supxrunb1  11612  supxrunb2  11613  ixxun  11658  ixxss1  11660  ixxss2  11661  ixxss12  11662  seqf1o  12260  faclbnd3  12483  rtrclreclem3  13123  sqrlem1  13306  sqrlem4  13309  sqrlem7  13312  abs3lemd  13522  rlimcn2  13653  o1of2  13675  lo1add  13689  lo1mul  13690  modfsummod  13853  mertenslem1  13939  sin01gt0  14243  cos01gt0  14244  sin02gt0  14245  dvds2subd  14335  bitsmod  14409  sadaddlem  14439  bezoutlem4OLD  14505  bezoutlem4  14508  mulgcd  14513  gcddvdslcm  14566  lcmgcdeq  14576  lcmfunsnlem2lem2  14611  isprm5  14650  mulgcddvds  14660  rpmulgcd2  14661  rpexp  14671  rpdvds  14675  phimullem  14726  eulerthlem1  14728  eulerthlem2  14729  prmdiv  14732  prmdiveq  14733  pythagtriplem4  14768  pcpremul  14792  pcqmul  14802  pcdvdstr  14824  pcgcd1  14825  pcadd  14833  pockthlem  14848  prmreclem2  14860  4sqlem8  14888  4sqlem10  14890  4sqlem14OLD  14901  4sqlem16OLD  14903  4sqlem14  14907  4sqlem16  14909  ramub1lem1  14983  ramub1lem2  14984  prmdvdsprmop  15000  prmgaplem1  15006  prmgaplcmlem1  15008  prmgaplcmlem1OLD  15011  prmdvdsprmorpOLD  15015  prmgaplem7  15026  iscatd2  15586  cicsym  15708  initoeu2  15910  joinval  16250  meetval  16264  lattrd  16303  latledi  16334  mulgass  16787  gaorber  16961  psgnunilem4  17137  efgredlem  17396  odadd2  17486  dmdprdpr  17681  ablfacrp2  17699  ablfac1b  17702  ablfac1eu  17705  pgpfac1  17712  gsumbagdiaglem  18598  znunit  19132  mdetunilem1  19635  mdetunilem4  19638  mdetunilem9  19643  neiptoptop  20145  lmcnp  20318  txcls  20617  txlly  20649  txnlly  20650  tx1stc  20663  alexsubALTlem1  21060  prdsmet  21383  blin2  21442  blcvx  21814  tgqioo  21816  metnrmlem3  21876  metnrmlem3OLD  21891  iscmet3lem2  22260  ovolmge0  22428  ovolunlem2  22449  mbfi1flimlem  22678  mbfmullem  22681  itg2add  22715  dvlip2  22945  dvge0  22956  dvcvx  22970  dvfsumabs  22973  plyadd  23169  plymul  23170  dgrlb  23188  plydivlem4  23247  vieta1lem2  23262  ulmdvlem3  23355  sinq12gt0  23460  logdivlti  23567  fsumharmonic  23935  fsumdvdsdiaglem  24110  dvdsmulf1o  24121  logfacubnd  24147  perfectlem1  24155  dchrptlem2  24191  lgsmod  24247  2sqlem3  24292  2sqlem5  24294  2sqlem8  24298  dchrisum0flblem2  24345  pntibndlem2  24427  pntlemr  24438  pntlemp  24446  axtgpasch  24513  wwlknredwwlkn  25452  wwlkextsur  25457  ex-natded5.2-2  25853  chscllem2  27289  chscllem4  27291  nmopge0  27562  nmfnge0  27578  nmoptrii  27745  staddi  27897  stadd3i  27899  atcvatlem  28036  supssd  28292  infssd  28293  xrofsup  28359  2sqmod  28416  xrge0addgt0  28461  archiabllem2c  28519  orngmul  28574  esumpmono  28908  unelldsys  28988  omssubaddlem  29135  signstfvneq0  29469  axtgupdim2OLD  29493  bnj1098  29603  bnj1110  29799  bnj1121  29802  erdszelem8  29929  txscon  29972  cvmlift2lem10  30043  cvmlift3lem7  30056  ghomgsg  30319  dvdspw  30393  dfon2lem6  30441  dfon2lem8  30443  cgrtr4d  30757  cgrtrand  30765  cgrtr3and  30767  cgrextendand  30781  btwnexch3and  30793  btwnexchand  30798  linecgrand  30854  endofsegidand  30858  btwnconn1lem4  30862  btwnconn1lem8  30866  btwnconn1lem11  30869  btwnconn1lem12  30870  brsegle2  30881  seglecgr12im  30882  segleantisym  30887  colinbtwnle  30890  broutsideof2  30894  outsideoftr  30901  outsidele  30904  lineelsb2  30920  linethru  30925  gtinf  30980  relowlssretop  31730  heicant  31939  mbfresfi  31951  ftc1anclem6  31986  riotasv2d  32498  lcvnbtwn2  32562  lcvnbtwn3  32563  lcvexchlem4  32572  omlfh1N  32793  atlen0  32845  atlatmstc  32854  cvratlem  32955  lnnat  32961  2atlt  32973  athgt  32990  1cvratex  33007  ps-2  33012  llncmp  33056  llncvrlpln  33092  lplncmp  33096  lplncvrlvol  33150  lvolcmp  33151  dalemcea  33194  dalem-cly  33205  dalem10  33207  dalem17  33214  dalem25  33232  dalem38  33244  dalem44  33250  dalem55  33261  2atm2atN  33319  cdlema1N  33325  paddasslem5  33358  dalawlem3  33407  dalawlem7  33411  dalawlem11  33415  dalawlem12  33416  lhp0lt  33537  4atexlemc  33603  cdlemg33a  34242  cdlemg33  34247  cdlemk51  34489  dia2dimlem2  34602  dia2dimlem3  34603  dihmeetlem20N  34863  ismrcd2  35510  pellqrex  35696  jm2.17b  35781  dvdsacongtr  35804  jm2.26lem3  35826  jm2.27a  35830  jm2.27c  35832  fnwe2lem2  35879  fco2d  36571  addrcom  36798  0ellimcdiv  37670  stoweidlem15  37815  stoweidlem26  37826  stoweidlem28  37828  stoweidlem32  37833  stoweidlem44  37845  icceuelpart  38620  perfectALTVlem1  38713  bgoldbtbndlem2  38771  bgoldbtbndlem3  38772  usgr2edg  39074  copisnmnd  39428  assintopass  39469  lcoss  39850  islindeps2  39897  isldepslvec2  39899  difmodm1lt  39946
  Copyright terms: Public domain W3C validator