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

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

Syntax hints:   -> wi 4   /\ wa 359

This theorem is referenced by:  anass  631  anabss3  797  f1elima  5968  fnfvof  6276  oecl  6740  oaass  6763  oen0  6788  oeworde  6795  omabs  6849  oiiniseg  7458  cardinfima  7934  fpwwe2lem12  8472  ltmul12a  9822  uzindOLD  10320  uzind3OLD  10321  eluzp1m1  10465  lbzbi  10520  qreccl  10550  xrlttr  10689  quoremnn0  11192  incexc2  12573  mertens  12618  ndvdsadd  12883  nn0seqcvgd  13016  isprm3  13043  pcval  13173  prdsval  13633  evlfcl  14274  frgpup1  15362  frgpup3lem  15364  gsumval3  15469  gsumzoppg  15494  ablfaclem2  15599  gsumdixp  15670  psrass1lem  16397  psrass1  16424  neissex  17146  neiptopnei  17151  tx1stc  17635  kqreglem1  17726  xpstopnlem1  17794  alexsublem  18028  psmettri2  18293  metuel2  18562  icoopnst  18917  iocopnst  18918  volcn  19451  mbflimsup  19511  mbflim  19513  itg1addlem4  19544  itg1addlem5  19545  itg1climres  19559  limcflf  19721  dvcobr  19785  dvcnvlem  19813  dvfsumge  19859  mdegmullem  19954  plyeq0lem  20082  plypf1  20084  mtestbdd  20274  mbfulm  20275  fsumdvdscom  20923  muinv  20931  logfaclbnd  20959  logexprlim  20962  dchrinv  20998  lgsval3  21051  rpvmasum2  21159  dchrisum0lem1  21163  dchrisum0  21167  selberg  21195  selberg3lem1  21204  selberg34r  21218  pntsval2  21223  grpoidinvlem4  21748  ipblnfi  22310  shmodsi  22844  eighmorth  23420  kbass5  23576  kbass6  23577  dmdmd  23756  atom1d  23809  mdsymlem2  23860  mdsymlem3  23861  mdsymlem4  23862  mdsymlem5  23863  ofrn  24005  pstmxmet  24245  dya2iocnei  24585  rescon  24886  nocvxminlem  25558  nobndlem6  25565  colinearalg  25753  axeuclid  25806  axcontlem2  25808  axcontlem7  25813  ismblfin  26146  mbfposadd  26153  itg2gt0cn  26159  cover2  26305  indexa  26325  filbcmb  26332  seqpo  26341  incsequz  26342  isbnd2  26382  ghomco  26448  unichnidl  26531  isfldidl  26568  frlmgsum  27100  unxpwdom3  27124  dihvalc  31716  dihvalb  31720

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