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

Theorem anasss 628
Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)
Hypothesis
Ref Expression
anasss.1  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
Assertion
Ref Expression
anasss  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )

Proof of Theorem anasss
StepHypRef Expression
1 anasss.1 . . 3  |-  ( ( ( ph  /\  ps )  /\  ch )  ->  th )
21exp31 587 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp32 422 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  anass  630  anabss3  796  f1elima  5787  fnfvof  6090  oecl  6536  oaass  6559  oen0  6584  oeworde  6591  omabs  6645  suppr  7219  oiiniseg  7248  cardinfima  7724  fpwwe2lem12  8263  ltmul12a  9612  uzindOLD  10106  uzind3OLD  10107  eluzp1m1  10251  lbzbi  10306  qreccl  10336  xrlttr  10474  quoremnn0  10960  incexc2  12297  mertens  12342  ndvdsadd  12607  nn0seqcvgd  12740  isprm3  12767  pcval  12897  prdsval  13355  evlfcl  13996  frgpup1  15084  frgpup3lem  15086  gsumval3  15191  gsumzoppg  15216  ablfaclem2  15321  gsumdixp  15392  psrass1lem  16123  psrass1  16150  neissex  16864  tx1stc  17344  kqreglem1  17432  xpstopnlem1  17500  alexsublem  17738  icoopnst  18437  iocopnst  18438  volcn  18961  mbflimsup  19021  mbflim  19023  itg1addlem4  19054  itg1addlem5  19055  itg1climres  19069  limcflf  19231  dvcobr  19295  dvcnvlem  19323  dvfsumge  19369  mdegmullem  19464  plyeq0lem  19592  plypf1  19594  mbfulm  19782  fsumdvdscom  20425  muinv  20433  logfaclbnd  20461  logexprlim  20464  dchrinv  20500  lgsval3  20553  rpvmasum2  20661  dchrisum0lem1  20665  dchrisum0  20669  selberg  20697  selberg3lem1  20706  selberg34r  20720  pntsval2  20725  grpoidinvlem4  20874  ipblnfi  21434  shmodsi  21968  eighmorth  22544  kbass5  22700  kbass6  22701  dmdmd  22880  atom1d  22933  mdsymlem2  22984  mdsymlem3  22985  mdsymlem4  22986  mdsymlem5  22987  ofrn  23206  esumcst  23436  rescon  23777  nocvxminlem  24344  nobndlem6  24351  colinearalg  24538  axeuclid  24591  axcontlem2  24593  axcontlem7  24598  cover2  26358  indexa  26412  filbcmb  26432  seqpo  26457  incsequz  26458  isbnd2  26507  ghomco  26573  unichnidl  26656  isfldidl  26693  frlmgsum  27232  unxpwdom3  27256  dihvalc  31423  dihvalb  31427
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator