MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anasss Structured version   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  6001  fnfvof  6309  oecl  6773  oaass  6796  oen0  6821  oeworde  6828  omabs  6882  oiiniseg  7494  cardinfima  7970  fpwwe2lem12  8508  ltmul12a  9858  uzindOLD  10356  uzind3OLD  10357  eluzp1m1  10501  lbzbi  10556  qreccl  10586  xrlttr  10725  quoremnn0  11229  incexc2  12610  mertens  12655  ndvdsadd  12920  nn0seqcvgd  13053  isprm3  13080  pcval  13210  prdsval  13670  evlfcl  14311  frgpup1  15399  frgpup3lem  15401  gsumval3  15506  gsumzoppg  15531  ablfaclem2  15636  gsumdixp  15707  psrass1lem  16434  psrass1  16461  neissex  17183  neiptopnei  17188  tx1stc  17674  kqreglem1  17765  xpstopnlem1  17833  alexsublem  18067  psmettri2  18332  metuel2  18601  icoopnst  18956  iocopnst  18957  volcn  19490  mbflimsup  19550  mbflim  19552  itg1addlem4  19583  itg1addlem5  19584  itg1climres  19598  limcflf  19760  dvcobr  19824  dvcnvlem  19852  dvfsumge  19898  mdegmullem  19993  plyeq0lem  20121  plypf1  20123  mtestbdd  20313  mbfulm  20314  fsumdvdscom  20962  muinv  20970  logfaclbnd  20998  logexprlim  21001  dchrinv  21037  lgsval3  21090  rpvmasum2  21198  dchrisum0lem1  21202  dchrisum0  21206  selberg  21234  selberg3lem1  21243  selberg34r  21257  pntsval2  21262  grpoidinvlem4  21787  ipblnfi  22349  shmodsi  22883  eighmorth  23459  kbass5  23615  kbass6  23616  dmdmd  23795  atom1d  23848  mdsymlem2  23899  mdsymlem3  23900  mdsymlem4  23901  mdsymlem5  23902  ofrn  24044  pstmxmet  24284  dya2iocnei  24624  rescon  24925  nocvxminlem  25637  nobndlem6  25644  colinearalg  25841  axeuclid  25894  axcontlem2  25896  axcontlem7  25901  ismblfin  26237  mbfposadd  26244  itg2gt0cn  26250  ftc1anclem7  26276  ftc1anc  26278  cover2  26406  indexa  26426  filbcmb  26433  seqpo  26442  incsequz  26443  isbnd2  26483  ghomco  26549  unichnidl  26632  isfldidl  26669  frlmgsum  27200  unxpwdom3  27224  dihvalc  31968  dihvalb  31972
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