Theorem anasss 642

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

Step	Hyp	Ref	Expression
1		anasss.1	. . 3 |- ( ( ( ph /\ ps ) /\ ch ) -> th )
2	1	exp31 601	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp32 433	1 |- ( ( ph /\ ( ps /\ ch ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 369

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

This theorem is referenced by:  anass  644  anabss3  814  f1elima  5973  fnfvof  6332  oecl  6973  oaass  6996  oen0  7021  oeworde  7028  omabs  7082  oiiniseg  7743  cardinfima  8263  fpwwe2lem12  8804  ltmul12a  10181  uzindOLD  10732  uzind3OLD  10733  eluzp1m1  10880  lbzbi  10939  qreccl  10969  xrlttr  11113  elfzodifsumelfzo  11600  quoremnn0  11691  incexc2  13297  mertens  13342  ndvdsadd  13608  nn0seqcvgd  13741  isprm3  13768  pcval  13907  prdsval  14389  evlfcl  15028  frgpup1  16265  frgpup3lem  16267  gsumval3OLD  16375  gsumval3  16378  gsumzoppg  16432  gsumzoppgOLD  16433  ablfaclem2  16577  gsumdixpOLD  16690  gsumdixp  16691  psrass1lem  17425  psrass1  17456  frlmgsumOLD  18154  frlmgsum  18155  neissex  18690  neiptopnei  18695  tx1stc  19182  kqreglem1  19273  xpstopnlem1  19341  alexsublem  19575  psmettri2  19844  metuel2  20113  icoopnst  20470  iocopnst  20471  volcn  21045  mbflimsup  21103  mbflim  21105  itg1addlem4  21136  itg1addlem5  21137  itg1climres  21151  limcflf  21315  dvcobr  21379  dvcnvlem  21407  dvfsumge  21453  mdegmullem  21508  plyeq0lem  21637  plypf1  21639  mtestbdd  21829  mbfulm  21830  fsumdvdscom  22484  muinv  22492  logfaclbnd  22520  logexprlim  22523  dchrinv  22559  lgsval3  22612  rpvmasum2  22720  dchrisum0lem1  22724  dchrisum0  22728  selberg  22756  selberg3lem1  22765  selberg34r  22779  pntsval2  22784  ercgrg  22928  colinearalg  23091  axeuclid  23144  axcontlem2  23146  axcontlem7  23151  grpoidinvlem4  23629  ipblnfi  24191  shmodsi  24727  eighmorth  25303  kbass5  25459  kbass6  25460  dmdmd  25639  atom1d  25692  mdsymlem2  25743  mdsymlem3  25744  mdsymlem4  25745  mdsymlem5  25746  ofrn  25892  gsummpt2co  26184  suborng  26218  pstmxmet  26260  ordtconlem1  26290  dya2iocnei  26633  rescon  27065  nocvxminlem  27760  nobndlem6  27767  fin2so  28341  ismblfin  28357  mbfposadd  28364  itg2gt0cn  28372  ftc1anclem7  28398  ftc1anc  28400  cover2  28532  indexa  28552  filbcmb  28559  seqpo  28568  incsequz  28569  isbnd2  28607  ghomco  28673  unichnidl  28756  isfldidl  28793  dihvalc  34600  dihvalb  34604