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

Theorem anasss 629
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 588 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  th ) ) )
32imp32 423 1  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  anass  631  anabss3  797  f1elima  5949  fnfvof  6257  oecl  6718  oaass  6741  oen0  6766  oeworde  6773  omabs  6827  oiiniseg  7436  cardinfima  7912  fpwwe2lem12  8450  ltmul12a  9799  uzindOLD  10297  uzind3OLD  10298  eluzp1m1  10442  lbzbi  10497  qreccl  10527  xrlttr  10666  quoremnn0  11165  incexc2  12546  mertens  12591  ndvdsadd  12856  nn0seqcvgd  12989  isprm3  13016  pcval  13146  prdsval  13606  evlfcl  14247  frgpup1  15335  frgpup3lem  15337  gsumval3  15442  gsumzoppg  15467  ablfaclem2  15572  gsumdixp  15643  psrass1lem  16370  psrass1  16397  neissex  17115  neiptopnei  17120  tx1stc  17604  kqreglem1  17695  xpstopnlem1  17763  alexsublem  17997  metuel2  18486  icoopnst  18836  iocopnst  18837  volcn  19366  mbflimsup  19426  mbflim  19428  itg1addlem4  19459  itg1addlem5  19460  itg1climres  19474  limcflf  19636  dvcobr  19700  dvcnvlem  19728  dvfsumge  19774  mdegmullem  19869  plyeq0lem  19997  plypf1  19999  mtestbdd  20189  mbfulm  20190  fsumdvdscom  20838  muinv  20846  logfaclbnd  20874  logexprlim  20877  dchrinv  20913  lgsval3  20966  rpvmasum2  21074  dchrisum0lem1  21078  dchrisum0  21082  selberg  21110  selberg3lem1  21119  selberg34r  21133  pntsval2  21138  grpoidinvlem4  21644  ipblnfi  22206  shmodsi  22740  eighmorth  23316  kbass5  23472  kbass6  23473  dmdmd  23652  atom1d  23705  mdsymlem2  23756  mdsymlem3  23757  mdsymlem4  23758  mdsymlem5  23759  dya2iocnei  24427  rescon  24713  nocvxminlem  25369  nobndlem6  25376  colinearalg  25564  axeuclid  25617  axcontlem2  25619  axcontlem7  25624  itg2gt0cn  25961  cover2  26107  indexa  26127  filbcmb  26134  seqpo  26143  incsequz  26144  isbnd2  26184  ghomco  26250  unichnidl  26333  isfldidl  26370  frlmgsum  26902  unxpwdom3  26926  dihvalc  31349  dihvalb  31353
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 178  df-an 361
  Copyright terms: Public domain W3C validator