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  819  f1elima  5981  fnfvof  6338  oecl  6982  oaass  7005  oen0  7030  oeworde  7037  omabs  7091  oiiniseg  7752  cardinfima  8272  fpwwe2lem12  8813  ltmul12a  10190  uzindOLD  10741  uzind3OLD  10742  eluzp1m1  10889  lbzbi  10948  qreccl  10978  xrlttr  11122  elfzodifsumelfzo  11609  quoremnn0  11700  incexc2  13306  mertens  13351  ndvdsadd  13617  nn0seqcvgd  13750  isprm3  13777  pcval  13916  prdsval  14398  evlfcl  15037  frgpup1  16277  frgpup3lem  16279  gsumval3OLD  16387  gsumval3  16390  gsumzoppg  16445  gsumzoppgOLD  16446  ablfaclem2  16592  gsumdixpOLD  16705  gsumdixp  16706  psrass1lem  17452  psrass1  17483  frlmgsumOLD  18200  frlmgsum  18201  neissex  18736  neiptopnei  18741  tx1stc  19228  kqreglem1  19319  xpstopnlem1  19387  alexsublem  19621  psmettri2  19890  metuel2  20159  icoopnst  20516  iocopnst  20517  volcn  21091  mbflimsup  21149  mbflim  21151  itg1addlem4  21182  itg1addlem5  21183  itg1climres  21197  limcflf  21361  dvcobr  21425  dvcnvlem  21453  dvfsumge  21499  mdegmullem  21554  plyeq0lem  21683  plypf1  21685  mtestbdd  21875  mbfulm  21876  fsumdvdscom  22530  muinv  22538  logfaclbnd  22566  logexprlim  22569  dchrinv  22605  lgsval3  22658  rpvmasum2  22766  dchrisum0lem1  22770  dchrisum0  22774  selberg  22802  selberg3lem1  22811  selberg34r  22825  pntsval2  22830  ercgrg  22974  colinearalg  23161  axeuclid  23214  axcontlem2  23216  axcontlem7  23221  grpoidinvlem4  23699  ipblnfi  24261  shmodsi  24797  eighmorth  25373  kbass5  25529  kbass6  25530  dmdmd  25709  atom1d  25762  mdsymlem2  25813  mdsymlem3  25814  mdsymlem4  25815  mdsymlem5  25816  ofrn  25962  gsummpt2co  26254  suborng  26288  pstmxmet  26329  ordtconlem1  26359  dya2iocnei  26702  rescon  27140  nocvxminlem  27836  nobndlem6  27843  fin2so  28421  ismblfin  28437  mbfposadd  28444  itg2gt0cn  28452  ftc1anclem7  28478  ftc1anc  28480  cover2  28612  indexa  28632  filbcmb  28639  seqpo  28648  incsequz  28649  isbnd2  28687  ghomco  28753  unichnidl  28836  isfldidl  28873  dihvalc  34883  dihvalb  34887