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

Theorem mp2and 679
Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
Hypotheses
Ref Expression
mp2and.1
mp2and.2
mp2and.3
Assertion
Ref Expression
mp2and

Proof of Theorem mp2and
StepHypRef Expression
1 mp2and.2 . 2
2 mp2and.1 . . 3
3 mp2and.3 . . 3
42, 3mpand 675 . 2
51, 4mpd 15 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  reu2eqd  3296  ssnelpssd  3891  tfisi  6693  tfindsg2  6696  mpt2sn  6891  smoord  7055  oelimcl  7268  oeeui  7270  nnawordex  7305  omabs  7315  ertrd  7346  omxpenlem  7638  ixpfi2  7838  supmaxOLD  7946  oismo  7986  cantnflem1c  8127  cantnflem1  8129  cantnflem3  8131  cantnflem1cOLD  8150  cantnflem1OLD  8152  cantnflem3OLD  8153  infxpenc2  8420  infxpenc2OLD  8424  axdc2lem  8849  r1limwun  9135  letrd  9760  lelttrd  9761  ltletrd  9763  lttrd  9764  le2addd  10195  le2subd  10196  ltleaddd  10197  leltaddd  10198  lt2subd  10200  ltmul12a  10423  lemul12ad  10513  lemul12bd  10514  lt2halvesd  10811  uzind  10979  uztrn  11126  xrlttrd  11391  xrlelttrd  11392  xrltletrd  11393  xrletrd  11394  supxrunb1  11540  supxrunb2  11541  ixxun  11574  ixxss1  11576  ixxss2  11577  ixxss12  11578  seqf1o  12148  faclbnd3  12370  sqrlem1  13076  sqrlem4  13079  sqrlem7  13082  abs3lemd  13292  rlimcn2  13413  o1of2  13435  lo1add  13449  lo1mul  13450  modfsummod  13608  mertenslem1  13693  sin01gt0  13925  cos01gt0  13926  sin02gt0  13927  dvds2subd  14017  bitsmod  14086  sadaddlem  14116  bezoutlem4  14179  mulgcd  14184  mulgcddvds  14245  rpmulgcd2  14246  isprm5  14253  rpexp  14261  rpdvds  14265  phimullem  14309  eulerthlem1  14311  eulerthlem2  14312  prmdiv  14315  prmdiveq  14316  pythagtriplem4  14343  pcpremul  14367  pcqmul  14377  pcdvdstr  14399  pcgcd1  14400  pcadd  14408  pockthlem  14423  prmreclem2  14435  4sqlem8  14463  4sqlem10  14465  4sqlem14  14476  4sqlem16  14478  ramub1lem1  14544  ramub1lem2  14545  iscatd2  15078  joinval  15635  meetval  15649  lattrd  15688  latledi  15719  mulgass  16172  gaorber  16346  psgnunilem4  16522  efgredlem  16765  odadd2  16855  dmdprdpr  17098  ablfacrp2  17118  ablfac1b  17121  ablfac1eu  17124  pgpfac1  17131  gsumbagdiaglem  18027  znunit  18602  mdetunilem1  19114  mdetunilem4  19117  mdetunilem9  19122  neiptoptop  19632  lmcnp  19805  txcls  20105  txlly  20137  txnlly  20138  tx1stc  20151  alexsubALTlem1  20547  prdsmet  20873  blin2  20932  blcvx  21303  tgqioo  21305  metnrmlem3  21365  iscmet3lem2  21731  ovolmge0  21888  ovolunlem2  21909  mbfi1flimlem  22129  mbfmullem  22132  itg2add  22166  dvlip2  22396  dvge0  22407  dvcvx  22421  dvfsumabs  22424  plyadd  22614  plymul  22615  dgrlb  22633  plydivlem4  22692  vieta1lem2  22707  ulmdvlem3  22797  sinq12gt0  22900  logdivlti  23005  fsumharmonic  23341  fsumdvdsdiaglem  23459  dvdsmulf1o  23470  logfacubnd  23496  perfectlem1  23504  dchrptlem2  23540  lgsmod  23596  2sqlem3  23641  2sqlem5  23643  2sqlem8  23647  dchrisum0flblem2  23694  pntibndlem2  23776  pntlemr  23787  pntlemp  23795  axtgpasch  23864  axtgupdim2  23869  wwlknredwwlkn  24726  wwlkextsur  24731  ex-natded5.2-2  25126  chscllem2  26556  chscllem4  26558  nmopge0  26830  nmfnge0  26846  nmoptrii  27013  staddi  27165  stadd3i  27167  atcvatlem  27304  supssd  27527  xrofsup  27582  2sqmod  27636  xrge0addgt0  27681  archiabllem2c  27739  orngmul  27793  esumpmono  28085  signstfvneq0  28529  erdszelem8  28642  txscon  28686  cvmlift2lem10  28757  cvmlift3lem7  28770  ghomgsg  29033  relexpsucl  29055  relexpcnv  29056  relexpdm  29058  relexprn  29059  rtrclreclem.trans  29069  dvdspw  29175  dfon2lem6  29220  dfon2lem8  29222  cgrtr4d  29635  cgrtrand  29643  cgrtr3and  29645  cgrextendand  29659  btwnexch3and  29671  btwnexchand  29676  linecgrand  29732  endofsegidand  29736  btwnconn1lem4  29740  btwnconn1lem8  29744  btwnconn1lem11  29747  btwnconn1lem12  29748  brsegle2  29759  seglecgr12im  29760  segleantisym  29765  colinbtwnle  29768  broutsideof2  29772  outsideoftr  29779  outsidele  29782  lineelsb2  29798  linethru  29803  heicant  30049  mbfresfi  30061  ftc1anclem6  30095  gtinf  30137  ismrcd2  30631  pellqrex  30815  jm2.17b  30899  dvdsacongtr  30922  jm2.26lem3  30943  jm2.27a  30947  jm2.27c  30949  fnwe2lem2  30997  gcddvdslcm  31208  lcmgcdeq  31216  addrcom  31384  0ellimcdiv  31655  stoweidlem15  31797  stoweidlem26  31808  stoweidlem28  31810  stoweidlem32  31814  stoweidlem44  31826  copisnmnd  32497  assintopass  32538  cicsym  32588  initoeu2  32622  lcoss  33037  islindeps2  33084  isldepslvec2  33086  bnj1098  33842  bnj1110  34038  bnj1121  34041  riotasv2d  34688  lcvnbtwn2  34752  lcvnbtwn3  34753  lcvexchlem4  34762  omlfh1N  34983  atlen0  35035  atlatmstc  35044  cvratlem  35145  lnnat  35151  2atlt  35163  athgt  35180  1cvratex  35197  ps-2  35202  llncmp  35246  llncvrlpln  35282  lplncmp  35286  lplncvrlvol  35340  lvolcmp  35341  dalemcea  35384  dalem-cly  35395  dalem10  35397  dalem17  35404  dalem25  35422  dalem38  35434  dalem44  35440  dalem55  35451  2atm2atN  35509  cdlema1N  35515  paddasslem5  35548  dalawlem3  35597  dalawlem7  35601  dalawlem11  35605  dalawlem12  35606  lhp0lt  35727  4atexlemc  35793  cdlemg33a  36432  cdlemg33  36437  cdlemk51  36679  dia2dimlem2  36792  dia2dimlem3  36793  dihmeetlem20N  37053  fco2d  37975
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
  Copyright terms: Public domain W3C validator