Theorem anasss 657

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

Syntax hints:   -> wi 4   /\ wa 375

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 190  df-an 377

This theorem is referenced by:  anass  659  anabss3  837  f1elima  6188  fnfvof  6571  oecl  7264  oaass  7287  oen0  7312  oeworde  7319  omabs  7373  oiiniseg  8073  cardinfima  8553  fpwwe2lem12  9091  ltmul12a  10488  eluzp1m1  11210  lbzbi  11280  qreccl  11312  xrlttr  11467  elfzodifsumelfzo  12010  quoremnn0  12114  incexc2  13944  mertens  13990  ndvdsadd  14437  nn0seqcvgd  14577  isprm3  14681  pcval  14842  prdsval  15401  evlfcl  16155  frgpup1  17473  frgpup3lem  17475  ghmcmn  17520  gsumval3  17589  gsumzoppg  17625  ablfaclem2  17767  gsumdixp  17885  psrass1lem  18649  psrass1  18677  frlmgsum  19378  m2cpminvid2  19827  pmatcollpw2lem  19849  chcoeffeqlem  19957  neissex  20191  neiptopnei  20196  dissnlocfin  20592  tx1stc  20713  kqreglem1  20804  xpstopnlem1  20872  alexsublem  21107  metuel2  21628  icoopnst  22015  iocopnst  22016  volcn  22612  mbflimsup  22671  mbflimsupOLD  22672  mbflim  22674  itg1addlem4  22705  itg1addlem5  22706  itg1climres  22720  limcflf  22884  dvcobr  22948  dvcnvlem  22976  dvfsumge  23022  mdegmullem  23075  plyeq0lem  23212  plypf1  23214  mtestbdd  23408  mbfulm  23409  fsumdvdscom  24162  muinv  24170  logfaclbnd  24198  logexprlim  24201  dchrinv  24237  lgsval3  24290  rpvmasum2  24398  dchrisum0lem1  24402  dchrisum0  24406  selberg  24434  selberg3lem1  24443  selberg34r  24457  pntsval2  24462  iscgrglt  24607  ercgrg  24610  legso  24692  oppperpex  24843  outpasch  24845  hpgerlem  24855  trgcopyeu  24896  dfcgra2  24919  inaghl  24929  colinearalg  24988  axeuclid  25041  axcontlem2  25043  axcontlem7  25048  grpoidinvlem4  25983  ipblnfi  26545  shmodsi  27090  eighmorth  27665  kbass5  27821  kbass6  27822  dmdmd  28001  atom1d  28054  mdsymlem2  28105  mdsymlem3  28106  mdsymlem4  28107  mdsymlem5  28108  2sqmo  28458  gsummpt2co  28591  suborng  28626  pstmxmet  28748  ordtconlem1  28778  esumiun  28963  dya2iocnei  29152  omssubadd  29176  omssubaddOLD  29180  rescon  30017  nocvxminlem  30627  nobndlem6  30634  fin2so  31976  poimirlem6  31990  poimirlem7  31991  poimirlem25  32009  poimirlem28  32012  poimirlem31  32015  poimirlem32  32016  broucube  32018  ismblfin  32025  mbfposadd  32032  itg2gt0cn  32041  ftc1anclem7  32067  ftc1anc  32069  cover2  32084  indexa  32104  filbcmb  32111  seqpo  32120  incsequz  32121  isbnd2  32159  ghomco  32225  unichnidl  32308  isfldidl  32345  dihvalc  34845  dihvalb  34849  isprm7  36703  radcnvrat  36706  dvnprodlem2  37859  etransclem46  38182  aacllem  40812