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

Theorem mp2and 677
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 673 . 2  |-  ( ph  ->  ( ch  ->  th )
)
51, 4mpd 15 1  |-  ( ph  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  reu2eqd  3221  ssnelpssd  3807  tfisi  6592  tfindsg2  6595  mpt2sn  6790  smoord  6954  oelimcl  7167  oeeui  7169  nnawordex  7204  omabs  7214  ertrd  7245  omxpenlem  7537  ixpfi2  7733  supmaxOLD  7840  oismo  7880  cantnflem1c  8019  cantnflem1  8021  cantnflem3  8023  cantnflem1cOLD  8042  cantnflem1OLD  8044  cantnflem3OLD  8045  infxpenc2  8312  infxpenc2OLD  8316  axdc2lem  8741  r1limwun  9025  letrd  9650  lelttrd  9651  ltletrd  9653  lttrd  9654  le2addd  10087  le2subd  10088  ltleaddd  10089  leltaddd  10090  lt2subd  10092  ltmul12a  10315  lemul12ad  10404  lemul12bd  10405  lt2halvesd  10703  uzind  10871  uztrn  11017  xrlttrd  11283  xrlelttrd  11284  xrltletrd  11285  xrletrd  11286  supxrunb1  11432  supxrunb2  11433  ixxun  11466  ixxss1  11468  ixxss2  11469  ixxss12  11470  seqf1o  12051  faclbnd3  12272  rtrclreclem3  12895  sqrlem1  13078  sqrlem4  13081  sqrlem7  13084  abs3lemd  13294  rlimcn2  13415  o1of2  13437  lo1add  13451  lo1mul  13452  modfsummod  13610  mertenslem1  13695  sin01gt0  13927  cos01gt0  13928  sin02gt0  13929  dvds2subd  14019  bitsmod  14088  sadaddlem  14118  bezoutlem4  14181  mulgcd  14186  mulgcddvds  14247  rpmulgcd2  14248  isprm5  14255  rpexp  14263  rpdvds  14267  phimullem  14311  eulerthlem1  14313  eulerthlem2  14314  prmdiv  14317  prmdiveq  14318  pythagtriplem4  14345  pcpremul  14369  pcqmul  14379  pcdvdstr  14401  pcgcd1  14402  pcadd  14410  pockthlem  14425  prmreclem2  14437  4sqlem8  14465  4sqlem10  14467  4sqlem14  14478  4sqlem16  14480  ramub1lem1  14546  ramub1lem2  14547  iscatd2  15088  cicsym  15210  initoeu2  15412  joinval  15752  meetval  15766  lattrd  15805  latledi  15836  mulgass  16289  gaorber  16463  psgnunilem4  16639  efgredlem  16882  odadd2  16972  dmdprdpr  17211  ablfacrp2  17231  ablfac1b  17234  ablfac1eu  17237  pgpfac1  17244  gsumbagdiaglem  18140  znunit  18693  mdetunilem1  19199  mdetunilem4  19202  mdetunilem9  19207  neiptoptop  19718  lmcnp  19891  txcls  20190  txlly  20222  txnlly  20223  tx1stc  20236  alexsubALTlem1  20632  prdsmet  20958  blin2  21017  blcvx  21388  tgqioo  21390  metnrmlem3  21450  iscmet3lem2  21816  ovolmge0  21973  ovolunlem2  21994  mbfi1flimlem  22214  mbfmullem  22217  itg2add  22251  dvlip2  22481  dvge0  22492  dvcvx  22506  dvfsumabs  22509  plyadd  22699  plymul  22700  dgrlb  22718  plydivlem4  22777  vieta1lem2  22792  ulmdvlem3  22882  sinq12gt0  22985  logdivlti  23092  fsumharmonic  23458  fsumdvdsdiaglem  23576  dvdsmulf1o  23587  logfacubnd  23613  perfectlem1  23621  dchrptlem2  23657  lgsmod  23713  2sqlem3  23758  2sqlem5  23760  2sqlem8  23764  dchrisum0flblem2  23811  pntibndlem2  23893  pntlemr  23904  pntlemp  23912  axtgpasch  23981  axtgupdim2  23986  wwlknredwwlkn  24847  wwlkextsur  24852  ex-natded5.2-2  25247  chscllem2  26673  chscllem4  26675  nmopge0  26946  nmfnge0  26962  nmoptrii  27129  staddi  27281  stadd3i  27283  atcvatlem  27420  supssd  27675  xrofsup  27735  2sqmod  27789  xrge0addgt0  27834  archiabllem2c  27892  orngmul  27947  esumpmono  28227  signstfvneq0  28712  erdszelem8  28831  txscon  28875  cvmlift2lem10  28946  cvmlift3lem7  28959  ghomgsg  29222  dvdspw  29341  dfon2lem6  29385  dfon2lem8  29387  cgrtr4d  29788  cgrtrand  29796  cgrtr3and  29798  cgrextendand  29812  btwnexch3and  29824  btwnexchand  29829  linecgrand  29885  endofsegidand  29889  btwnconn1lem4  29893  btwnconn1lem8  29897  btwnconn1lem11  29900  btwnconn1lem12  29901  brsegle2  29912  seglecgr12im  29913  segleantisym  29918  colinbtwnle  29921  broutsideof2  29925  outsideoftr  29932  outsidele  29935  lineelsb2  29951  linethru  29956  heicant  30214  mbfresfi  30226  ftc1anclem6  30261  gtinf  30303  ismrcd2  30797  pellqrex  30980  jm2.17b  31064  dvdsacongtr  31087  jm2.26lem3  31109  jm2.27a  31113  jm2.27c  31115  fnwe2lem2  31163  gcddvdslcm  31376  lcmgcdeq  31384  addrcom  31552  0ellimcdiv  31821  stoweidlem15  31963  stoweidlem26  31974  stoweidlem28  31976  stoweidlem32  31980  stoweidlem44  31992  perfectALTVlem1  32543  copisnmnd  32815  assintopass  32856  lcoss  33237  islindeps2  33284  isldepslvec2  33286  difmodm1lt  33335  bnj1098  34189  bnj1110  34385  bnj1121  34388  riotasv2d  35101  lcvnbtwn2  35165  lcvnbtwn3  35166  lcvexchlem4  35175  omlfh1N  35396  atlen0  35448  atlatmstc  35457  cvratlem  35558  lnnat  35564  2atlt  35576  athgt  35593  1cvratex  35610  ps-2  35615  llncmp  35659  llncvrlpln  35695  lplncmp  35699  lplncvrlvol  35753  lvolcmp  35754  dalemcea  35797  dalem-cly  35808  dalem10  35810  dalem17  35817  dalem25  35835  dalem38  35847  dalem44  35853  dalem55  35864  2atm2atN  35922  cdlema1N  35928  paddasslem5  35961  dalawlem3  36010  dalawlem7  36014  dalawlem11  36018  dalawlem12  36019  lhp0lt  36140  4atexlemc  36206  cdlemg33a  36845  cdlemg33  36850  cdlemk51  37092  dia2dimlem2  37205  dia2dimlem3  37206  dihmeetlem20N  37466  fco2d  38504
  Copyright terms: Public domain W3C validator