Theorem anasss 651

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

Syntax hints:   -> wi 4   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  anass  653  anabss3  830  f1elima  6123  fnfvof  6503  oecl  7194  oaass  7217  oen0  7242  oeworde  7249  omabs  7303  oiiniseg  8001  cardinfima  8479  fpwwe2lem12  9017  ltmul12a  10412  eluzp1m1  11133  lbzbi  11203  qreccl  11235  xrlttr  11390  elfzodifsumelfzo  11930  quoremnn0  12033  incexc2  13839  mertens  13885  ndvdsadd  14332  nn0seqcvgd  14472  isprm3  14576  pcval  14737  prdsval  15296  evlfcl  16050  frgpup1  17368  frgpup3lem  17370  ghmcmn  17415  gsumval3  17484  gsumzoppg  17520  ablfaclem2  17662  gsumdixp  17780  psrass1lem  18544  psrass1  18572  frlmgsum  19272  m2cpminvid2  19721  pmatcollpw2lem  19743  chcoeffeqlem  19851  neissex  20085  neiptopnei  20090  dissnlocfin  20486  tx1stc  20607  kqreglem1  20698  xpstopnlem1  20766  alexsublem  21001  metuel2  21522  icoopnst  21909  iocopnst  21910  volcn  22506  mbflimsup  22565  mbflimsupOLD  22566  mbflim  22568  itg1addlem4  22599  itg1addlem5  22600  itg1climres  22614  limcflf  22778  dvcobr  22842  dvcnvlem  22870  dvfsumge  22916  mdegmullem  22969  plyeq0lem  23106  plypf1  23108  mtestbdd  23302  mbfulm  23303  fsumdvdscom  24056  muinv  24064  logfaclbnd  24092  logexprlim  24095  dchrinv  24131  lgsval3  24184  rpvmasum2  24292  dchrisum0lem1  24296  dchrisum0  24300  selberg  24328  selberg3lem1  24337  selberg34r  24351  pntsval2  24356  iscgrglt  24501  ercgrg  24504  legso  24586  oppperpex  24737  outpasch  24739  hpgerlem  24749  trgcopyeu  24790  dfcgra2  24813  inaghl  24823  colinearalg  24882  axeuclid  24935  axcontlem2  24937  axcontlem7  24942  grpoidinvlem4  25877  ipblnfi  26439  shmodsi  26984  eighmorth  27559  kbass5  27715  kbass6  27716  dmdmd  27895  atom1d  27948  mdsymlem2  27999  mdsymlem3  28000  mdsymlem4  28001  mdsymlem5  28002  2sqmo  28361  gsummpt2co  28494  suborng  28530  pstmxmet  28652  ordtconlem1  28682  esumiun  28867  dya2iocnei  29056  omssubadd  29080  omssubaddOLD  29084  rescon  29921  nocvxminlem  30528  nobndlem6  30535  fin2so  31839  poimirlem6  31853  poimirlem7  31854  poimirlem25  31872  poimirlem28  31875  poimirlem31  31878  poimirlem32  31879  broucube  31881  ismblfin  31888  mbfposadd  31895  itg2gt0cn  31904  ftc1anclem7  31930  ftc1anc  31932  cover2  31947  indexa  31967  filbcmb  31974  seqpo  31983  incsequz  31984  isbnd2  32022  ghomco  32088  unichnidl  32171  isfldidl  32208  dihvalc  34713  dihvalb  34717  isprm7  36573  radcnvrat  36576  dvnprodlem2  37705  etransclem46  38028  aacllem  40133