Theorem anasss 645

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 602	. 2 |- ( ph -> ( ps -> ( ch -> th ) ) )
3	2	imp32 431	1 |- ( ( ph /\ ( ps /\ ch ) ) -> th )

Syntax hints:   -> wi 4   /\ wa 367

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 369

This theorem is referenced by:  anass  647  anabss3  821  f1elima  6146  fnfvof  6526  oecl  7179  oaass  7202  oen0  7227  oeworde  7234  omabs  7288  oiiniseg  7950  cardinfima  8469  fpwwe2lem12  9008  ltmul12a  10394  uzindOLD  10953  uzind3OLD  10954  eluzp1m1  11105  lbzbi  11171  qreccl  11203  xrlttr  11349  elfzodifsumelfzo  11863  quoremnn0  11965  incexc2  13732  mertens  13777  ndvdsadd  14150  nn0seqcvgd  14283  isprm3  14310  pcval  14452  prdsval  14944  evlfcl  15690  frgpup1  16992  frgpup3lem  16994  ghmcmn  17039  gsumval3OLD  17107  gsumval3  17110  gsumzoppg  17165  gsumzoppgOLD  17166  ablfaclem2  17332  gsumdixpOLD  17452  gsumdixp  17453  psrass1lem  18224  psrass1  18255  frlmgsumOLD  18972  frlmgsum  18973  m2cpminvid2  19423  pmatcollpw2lem  19445  chcoeffeqlem  19553  neissex  19795  neiptopnei  19800  dissnlocfin  20196  tx1stc  20317  kqreglem1  20408  xpstopnlem1  20476  alexsublem  20710  metuel2  21248  icoopnst  21605  iocopnst  21606  volcn  22181  mbflimsup  22239  mbflim  22241  itg1addlem4  22272  itg1addlem5  22273  itg1climres  22287  limcflf  22451  dvcobr  22515  dvcnvlem  22543  dvfsumge  22589  mdegmullem  22644  plyeq0lem  22773  plypf1  22775  mtestbdd  22966  mbfulm  22967  fsumdvdscom  23659  muinv  23667  logfaclbnd  23695  logexprlim  23698  dchrinv  23734  lgsval3  23787  rpvmasum2  23895  dchrisum0lem1  23899  dchrisum0  23903  selberg  23931  selberg3lem1  23940  selberg34r  23954  pntsval2  23959  ercgrg  24109  legso  24186  hpgerlem  24335  colinearalg  24415  axeuclid  24468  axcontlem2  24470  axcontlem7  24475  grpoidinvlem4  25407  ipblnfi  25969  shmodsi  26505  eighmorth  27081  kbass5  27237  kbass6  27238  dmdmd  27417  atom1d  27470  mdsymlem2  27521  mdsymlem3  27522  mdsymlem4  27523  mdsymlem5  27524  2sqmo  27871  gsummpt2co  28005  suborng  28040  pstmxmet  28111  ordtconlem1  28141  esumiun  28323  dya2iocnei  28490  omssubadd  28508  rescon  28955  nocvxminlem  29690  nobndlem6  29697  fin2so  30280  ismblfin  30295  mbfposadd  30302  itg2gt0cn  30310  ftc1anclem7  30336  ftc1anc  30338  cover2  30444  indexa  30464  filbcmb  30471  seqpo  30480  incsequz  30481  isbnd2  30519  ghomco  30585  unichnidl  30668  isfldidl  30705  isprm7  31433  radcnvrat  31436  dvnprodlem2  31983  etransclem46  32302  aacllem  33604  dihvalc  37357  dihvalb  37361