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  3274  ssnelpssd  3864  tfisi  6699  tfindsg2  6702  mpt2sn  6898  smoord  7092  oelimcl  7309  oeeui  7311  nnawordex  7346  omabs  7356  ertrd  7387  omxpenlem  7679  ixpfi2  7878  supmaxOLD  7989  oismo  8055  cantnflem1c  8191  cantnflem1  8193  cantnflem3  8195  infxpenc2  8451  axdc2lem  8876  r1limwun  9160  letrd  9791  lelttrd  9792  ltletrd  9794  lttrd  9795  le2addd  10231  le2subd  10232  ltleaddd  10233  leltaddd  10234  lt2subd  10236  ltmul12a  10460  lemul12ad  10549  lemul12bd  10550  lt2halvesd  10860  uzind  11027  uztrn  11175  xrlttrd  11456  xrlelttrd  11457  xrltletrd  11458  xrletrd  11459  supxrunb1  11605  supxrunb2  11606  ixxun  11651  ixxss1  11653  ixxss2  11654  ixxss12  11655  seqf1o  12251  faclbnd3  12474  rtrclreclem3  13102  sqrlem1  13285  sqrlem4  13288  sqrlem7  13291  abs3lemd  13501  rlimcn2  13632  o1of2  13654  lo1add  13668  lo1mul  13669  modfsummod  13832  mertenslem1  13918  sin01gt0  14222  cos01gt0  14223  sin02gt0  14224  dvds2subd  14314  bitsmod  14384  sadaddlem  14414  bezoutlem4  14480  mulgcd  14485  gcddvdslcm  14532  lcmgcdeq  14542  lcmfunsnlem2lem2  14574  isprm5  14613  mulgcddvds  14623  rpmulgcd2  14624  rpexp  14634  rpdvds  14638  phimullem  14687  eulerthlem1  14689  eulerthlem2  14690  prmdiv  14693  prmdiveq  14694  pythagtriplem4  14723  pcpremul  14747  pcqmul  14757  pcdvdstr  14779  pcgcd1  14780  pcadd  14788  pockthlem  14803  prmreclem2  14815  4sqlem8  14843  4sqlem10  14845  4sqlem14OLD  14856  4sqlem16OLD  14858  4sqlem14  14862  4sqlem16  14864  ramub1lem1  14938  ramub1lem2  14939  prmdvdsprmop  14955  prmgaplem1  14961  prmgaplcmlem1  14963  prmgaplcmlem1OLD  14966  prmdvdsprmorpOLD  14970  prmgaplem7  14981  iscatd2  15529  cicsym  15651  initoeu2  15853  joinval  16193  meetval  16207  lattrd  16246  latledi  16277  mulgass  16730  gaorber  16904  psgnunilem4  17080  efgredlem  17323  odadd2  17413  dmdprdpr  17608  ablfacrp2  17626  ablfac1b  17629  ablfac1eu  17632  pgpfac1  17639  gsumbagdiaglem  18525  znunit  19056  mdetunilem1  19559  mdetunilem4  19562  mdetunilem9  19567  neiptoptop  20069  lmcnp  20242  txcls  20541  txlly  20573  txnlly  20574  tx1stc  20587  alexsubALTlem1  20984  prdsmet  21307  blin2  21366  blcvx  21718  tgqioo  21720  metnrmlem3  21780  iscmet3lem2  22146  ovolmge0  22299  ovolunlem2  22320  mbfi1flimlem  22548  mbfmullem  22551  itg2add  22585  dvlip2  22815  dvge0  22826  dvcvx  22840  dvfsumabs  22843  plyadd  23030  plymul  23031  dgrlb  23049  plydivlem4  23108  vieta1lem2  23123  ulmdvlem3  23213  sinq12gt0  23318  logdivlti  23425  fsumharmonic  23793  fsumdvdsdiaglem  23966  dvdsmulf1o  23977  logfacubnd  24003  perfectlem1  24011  dchrptlem2  24047  lgsmod  24103  2sqlem3  24148  2sqlem5  24150  2sqlem8  24154  dchrisum0flblem2  24201  pntibndlem2  24283  pntlemr  24294  pntlemp  24302  axtgpasch  24369  wwlknredwwlkn  25290  wwlkextsur  25295  ex-natded5.2-2  25691  chscllem2  27117  chscllem4  27119  nmopge0  27390  nmfnge0  27406  nmoptrii  27573  staddi  27725  stadd3i  27727  atcvatlem  27864  supssd  28121  xrofsup  28180  2sqmod  28238  xrge0addgt0  28283  archiabllem2c  28341  orngmul  28396  esumpmono  28730  unelldsys  28810  signstfvneq0  29240  axtgupdim2OLD  29264  bnj1098  29374  bnj1110  29570  bnj1121  29573  erdszelem8  29700  txscon  29743  cvmlift2lem10  29814  cvmlift3lem7  29827  ghomgsg  30090  dvdspw  30164  dfon2lem6  30212  dfon2lem8  30214  cgrtr4d  30528  cgrtrand  30536  cgrtr3and  30538  cgrextendand  30552  btwnexch3and  30564  btwnexchand  30569  linecgrand  30625  endofsegidand  30629  btwnconn1lem4  30633  btwnconn1lem8  30637  btwnconn1lem11  30640  btwnconn1lem12  30641  brsegle2  30652  seglecgr12im  30653  segleantisym  30658  colinbtwnle  30661  broutsideof2  30665  outsideoftr  30672  outsidele  30675  lineelsb2  30691  linethru  30696  gtinf  30751  relowlssretop  31491  heicant  31669  mbfresfi  31681  ftc1anclem6  31716  riotasv2d  32228  lcvnbtwn2  32292  lcvnbtwn3  32293  lcvexchlem4  32302  omlfh1N  32523  atlen0  32575  atlatmstc  32584  cvratlem  32685  lnnat  32691  2atlt  32703  athgt  32720  1cvratex  32737  ps-2  32742  llncmp  32786  llncvrlpln  32822  lplncmp  32826  lplncvrlvol  32880  lvolcmp  32881  dalemcea  32924  dalem-cly  32935  dalem10  32937  dalem17  32944  dalem25  32962  dalem38  32974  dalem44  32980  dalem55  32991  2atm2atN  33049  cdlema1N  33055  paddasslem5  33088  dalawlem3  33137  dalawlem7  33141  dalawlem11  33145  dalawlem12  33146  lhp0lt  33267  4atexlemc  33333  cdlemg33a  33972  cdlemg33  33977  cdlemk51  34219  dia2dimlem2  34332  dia2dimlem3  34333  dihmeetlem20N  34593  ismrcd2  35240  pellqrex  35423  jm2.17b  35507  dvdsacongtr  35530  jm2.26lem3  35552  jm2.27a  35556  jm2.27c  35558  fnwe2lem2  35605  fco2d  36228  addrcom  36455  0ellimcdiv  37292  stoweidlem15  37434  stoweidlem26  37445  stoweidlem28  37447  stoweidlem32  37452  stoweidlem44  37464  icceuelpart  38130  perfectALTVlem1  38223  bgoldbtbndlem2  38281  bgoldbtbndlem3  38282  copisnmnd  38557  assintopass  38598  lcoss  38979  islindeps2  39026  isldepslvec2  39028  difmodm1lt  39076
  Copyright terms: Public domain W3C validator