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

Theorem mp2and 693
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 689 . 2  |-  ( ph  ->  ( ch  ->  th )
)
51, 4mpd 15 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376
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 190  df-an 378
This theorem is referenced by:  reu2eqd  3223  ssnelpssd  3531  tfisi  6704  tfindsg2  6707  mpt2sn  6906  smoord  7102  oelimcl  7319  oeeui  7321  nnawordex  7356  omabs  7366  ertrd  7397  omxpenlem  7691  ixpfi2  7890  supmaxOLD  8001  oismo  8073  cantnflem1c  8210  cantnflem1  8212  cantnflem3  8214  infxpenc2  8471  axdc2lem  8896  r1limwun  9179  letrd  9809  lelttrd  9810  ltletrd  9812  lttrd  9813  le2addd  10253  le2subd  10254  ltleaddd  10255  leltaddd  10256  lt2subd  10258  ltmul12a  10483  lemul12ad  10571  lemul12bd  10572  lt2halvesd  10883  uzind  11050  uztrn  11199  xrlttrd  11479  xrlelttrd  11480  xrltletrd  11481  xrletrd  11482  supxrunb1  11630  supxrunb2  11631  ixxun  11676  ixxss1  11678  ixxss2  11679  ixxss12  11680  seqf1o  12292  faclbnd3  12515  rtrclreclem3  13200  sqrlem1  13383  sqrlem4  13386  sqrlem7  13389  abs3lemd  13600  rlimcn2  13731  o1of2  13753  lo1add  13767  lo1mul  13768  modfsummod  13931  mertenslem1  14017  sin01gt0  14321  cos01gt0  14322  sin02gt0  14323  dvds2subd  14413  bitsmod  14489  sadaddlem  14519  bezoutlem4OLD  14585  bezoutlem4  14588  mulgcd  14593  gcddvdslcm  14646  lcmgcdeq  14656  lcmfunsnlem2lem2  14691  isprm5  14730  mulgcddvds  14740  rpmulgcd2  14741  rpexp  14751  rpdvds  14755  phimullem  14806  eulerthlem1  14808  eulerthlem2  14809  prmdiv  14812  prmdiveq  14813  pythagtriplem4  14848  pcpremul  14872  pcqmul  14882  pcdvdstr  14904  pcgcd1  14905  pcadd  14913  pockthlem  14928  prmreclem2  14940  4sqlem8  14968  4sqlem10  14970  4sqlem14OLD  14981  4sqlem16OLD  14983  4sqlem14  14987  4sqlem16  14989  ramub1lem1  15063  ramub1lem2  15064  prmdvdsprmop  15080  prmgaplem1  15086  prmgaplcmlem1  15088  prmgaplcmlem1OLD  15091  prmdvdsprmorpOLD  15095  prmgaplem7  15106  iscatd2  15665  cicsym  15787  initoeu2  15989  joinval  16329  meetval  16343  lattrd  16382  latledi  16413  mulgass  16866  gaorber  17040  psgnunilem4  17216  efgredlem  17475  odadd2  17565  dmdprdpr  17760  ablfacrp2  17778  ablfac1b  17781  ablfac1eu  17784  pgpfac1  17791  gsumbagdiaglem  18676  znunit  19211  mdetunilem1  19714  mdetunilem4  19717  mdetunilem9  19722  neiptoptop  20224  lmcnp  20397  txcls  20696  txlly  20728  txnlly  20729  tx1stc  20742  alexsubALTlem1  21140  prdsmet  21463  blin2  21522  blcvx  21894  tgqioo  21896  metnrmlem3  21956  metnrmlem3OLD  21971  iscmet3lem2  22340  ovolmge0  22508  ovolunlem2  22529  mbfi1flimlem  22759  mbfmullem  22762  itg2add  22796  dvlip2  23026  dvge0  23037  dvcvx  23051  dvfsumabs  23054  plyadd  23250  plymul  23251  dgrlb  23269  plydivlem4  23328  vieta1lem2  23343  ulmdvlem3  23436  sinq12gt0  23541  logdivlti  23648  fsumharmonic  24016  fsumdvdsdiaglem  24191  dvdsmulf1o  24202  logfacubnd  24228  perfectlem1  24236  dchrptlem2  24272  lgsmod  24328  2sqlem3  24373  2sqlem5  24375  2sqlem8  24379  dchrisum0flblem2  24426  pntibndlem2  24508  pntlemr  24519  pntlemp  24527  axtgpasch  24594  wwlknredwwlkn  25533  wwlkextsur  25538  ex-natded5.2-2  25934  chscllem2  27372  chscllem4  27374  nmopge0  27645  nmfnge0  27661  nmoptrii  27828  staddi  27980  stadd3i  27982  atcvatlem  28119  supssd  28365  infssd  28366  xrofsup  28428  2sqmod  28484  xrge0addgt0  28528  archiabllem2c  28586  orngmul  28640  esumpmono  28974  unelldsys  29054  omssubaddlem  29200  signstfvneq0  29533  axtgupdim2OLD  29557  bnj1098  29667  bnj1110  29863  bnj1121  29866  erdszelem8  29993  txscon  30036  cvmlift2lem10  30107  cvmlift3lem7  30120  ghomgsg  30383  dvdspw  30457  dfon2lem6  30505  dfon2lem8  30507  cgrtr4d  30823  cgrtrand  30831  cgrtr3and  30833  cgrextendand  30847  btwnexch3and  30859  btwnexchand  30864  linecgrand  30920  endofsegidand  30924  btwnconn1lem4  30928  btwnconn1lem8  30932  btwnconn1lem11  30935  btwnconn1lem12  30936  brsegle2  30947  seglecgr12im  30948  segleantisym  30953  colinbtwnle  30956  broutsideof2  30960  outsideoftr  30967  outsidele  30970  lineelsb2  30986  linethru  30991  gtinf  31046  relowlssretop  31836  heicant  32039  mbfresfi  32051  ftc1anclem6  32086  riotasv2d  32593  lcvnbtwn2  32664  lcvnbtwn3  32665  lcvexchlem4  32674  omlfh1N  32895  atlen0  32947  atlatmstc  32956  cvratlem  33057  lnnat  33063  2atlt  33075  athgt  33092  1cvratex  33109  ps-2  33114  llncmp  33158  llncvrlpln  33194  lplncmp  33198  lplncvrlvol  33252  lvolcmp  33253  dalemcea  33296  dalem-cly  33307  dalem10  33309  dalem17  33316  dalem25  33334  dalem38  33346  dalem44  33352  dalem55  33363  2atm2atN  33421  cdlema1N  33427  paddasslem5  33460  dalawlem3  33509  dalawlem7  33513  dalawlem11  33517  dalawlem12  33518  lhp0lt  33639  4atexlemc  33705  cdlemg33a  34344  cdlemg33  34349  cdlemk51  34591  dia2dimlem2  34704  dia2dimlem3  34705  dihmeetlem20N  34965  ismrcd2  35612  pellqrex  35797  jm2.17b  35882  dvdsacongtr  35905  jm2.26lem3  35927  jm2.27a  35931  jm2.27c  35933  fnwe2lem2  35980  fco2d  36672  addrcom  36898  infxrunb2  37678  0ellimcdiv  37827  stoweidlem15  37987  stoweidlem26  37998  stoweidlem28  38000  stoweidlem32  38005  stoweidlem44  38017  icceuelpart  38895  perfectALTVlem1  38988  bgoldbtbndlem2  39046  bgoldbtbndlem3  39047  1wlkcompim  39834  upgr4cycl4dv4e  40099  copisnmnd  40317  assintopass  40358  lcoss  40737  islindeps2  40784  isldepslvec2  40786  difmodm1lt  40833
  Copyright terms: Public domain W3C validator