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

Theorem anasss 647
Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)
Hypothesis
Ref Expression
anasss.1
Assertion
Ref Expression
anasss

Proof of Theorem anasss
StepHypRef Expression
1 anasss.1 . . 3
21exp31 604 . 2
32imp32 433 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  anass  649  anabss3  823  f1elima  6171  fnfvof  6553  oecl  7206  oaass  7229  oen0  7254  oeworde  7261  omabs  7315  oiiniseg  7979  cardinfima  8499  fpwwe2lem12  9040  ltmul12a  10423  uzindOLD  10982  uzind3OLD  10983  eluzp1m1  11133  lbzbi  11199  qreccl  11231  xrlttr  11375  elfzodifsumelfzo  11882  quoremnn0  11983  incexc2  13650  mertens  13695  ndvdsadd  14066  nn0seqcvgd  14199  isprm3  14226  pcval  14368  prdsval  14852  evlfcl  15491  frgpup1  16793  frgpup3lem  16795  ghmcmn  16840  gsumval3OLD  16908  gsumval3  16911  gsumzoppg  16967  gsumzoppgOLD  16968  ablfaclem2  17137  gsumdixpOLD  17257  gsumdixp  17258  psrass1lem  18029  psrass1  18060  frlmgsumOLD  18801  frlmgsum  18802  m2cpminvid2  19256  pmatcollpw2lem  19278  chcoeffeqlem  19386  neissex  19628  neiptopnei  19633  dissnlocfin  20030  tx1stc  20151  kqreglem1  20242  xpstopnlem1  20310  alexsublem  20544  metuel2  21082  icoopnst  21439  iocopnst  21440  volcn  22015  mbflimsup  22073  mbflim  22075  itg1addlem4  22106  itg1addlem5  22107  itg1climres  22121  limcflf  22285  dvcobr  22349  dvcnvlem  22377  dvfsumge  22423  mdegmullem  22478  plyeq0lem  22607  plypf1  22609  mtestbdd  22800  mbfulm  22801  fsumdvdscom  23461  muinv  23469  logfaclbnd  23497  logexprlim  23500  dchrinv  23536  lgsval3  23589  rpvmasum2  23697  dchrisum0lem1  23701  dchrisum0  23705  selberg  23733  selberg3lem1  23742  selberg34r  23756  pntsval2  23761  ercgrg  23908  legso  23985  hpgerlem  24134  colinearalg  24213  axeuclid  24266  axcontlem2  24268  axcontlem7  24273  grpoidinvlem4  25209  ipblnfi  25771  shmodsi  26307  eighmorth  26883  kbass5  27039  kbass6  27040  dmdmd  27219  atom1d  27272  mdsymlem2  27323  mdsymlem3  27324  mdsymlem4  27325  mdsymlem5  27326  2sqmo  27637  gsummpt2co  27771  suborng  27805  pstmxmet  27876  ordtconlem1  27906  dya2iocnei  28253  rescon  28691  nocvxminlem  29450  nobndlem6  29457  fin2so  30040  ismblfin  30055  mbfposadd  30062  itg2gt0cn  30070  ftc1anclem7  30096  ftc1anc  30098  cover2  30204  indexa  30224  filbcmb  30231  seqpo  30240  incsequz  30241  isbnd2  30279  ghomco  30345  unichnidl  30428  isfldidl  30465  isprm7  31192  radcnvrat  31195  dvnprodlem2  31744  etransclem46  32063  aacllem  33216  dihvalc  36960  dihvalb  36964
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