Theorem anasss 647

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 604	. 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  649  anabss3  823  f1elima  6156  fnfvof  6538  oecl  7189  oaass  7212  oen0  7237  oeworde  7244  omabs  7298  oiiniseg  7961  cardinfima  8481  fpwwe2lem12  9022  ltmul12a  10404  uzindOLD  10963  uzind3OLD  10964  eluzp1m1  11113  lbzbi  11179  qreccl  11211  xrlttr  11355  elfzodifsumelfzo  11861  quoremnn0  11962  incexc2  13629  mertens  13674  ndvdsadd  13943  nn0seqcvgd  14076  isprm3  14103  pcval  14245  prdsval  14729  evlfcl  15365  frgpup1  16667  frgpup3lem  16669  ghmcmn  16714  gsumval3OLD  16782  gsumval3  16785  gsumzoppg  16841  gsumzoppgOLD  16842  ablfaclem2  17011  gsumdixpOLD  17131  gsumdixp  17132  psrass1lem  17903  psrass1  17934  frlmgsumOLD  18674  frlmgsum  18675  m2cpminvid2  19129  pmatcollpw2lem  19151  chcoeffeqlem  19259  neissex  19501  neiptopnei  19506  dissnlocfin  19903  tx1stc  20024  kqreglem1  20115  xpstopnlem1  20183  alexsublem  20417  metuel2  20955  icoopnst  21312  iocopnst  21313  volcn  21888  mbflimsup  21946  mbflim  21948  itg1addlem4  21979  itg1addlem5  21980  itg1climres  21994  limcflf  22158  dvcobr  22222  dvcnvlem  22250  dvfsumge  22296  mdegmullem  22351  plyeq0lem  22480  plypf1  22482  mtestbdd  22672  mbfulm  22673  fsumdvdscom  23333  muinv  23341  logfaclbnd  23369  logexprlim  23372  dchrinv  23408  lgsval3  23461  rpvmasum2  23569  dchrisum0lem1  23573  dchrisum0  23577  selberg  23605  selberg3lem1  23614  selberg34r  23628  pntsval2  23633  ercgrg  23780  legso  23857  hpgerlem  24006  colinearalg  24085  axeuclid  24138  axcontlem2  24140  axcontlem7  24145  grpoidinvlem4  25081  ipblnfi  25643  shmodsi  26179  eighmorth  26755  kbass5  26911  kbass6  26912  dmdmd  27091  atom1d  27144  mdsymlem2  27195  mdsymlem3  27196  mdsymlem4  27197  mdsymlem5  27198  2sqmo  27510  gsummpt2co  27644  suborng  27678  pstmxmet  27749  ordtconlem1  27779  dya2iocnei  28126  rescon  28564  nocvxminlem  29425  nobndlem6  29432  fin2so  30015  ismblfin  30030  mbfposadd  30037  itg2gt0cn  30045  ftc1anclem7  30071  ftc1anc  30073  cover2  30179  indexa  30199  filbcmb  30206  seqpo  30215  incsequz  30216  isbnd2  30254  ghomco  30320  unichnidl  30403  isfldidl  30440  isprm7  31168  radcnvrat  31171  dihvalc  36700  dihvalb  36704