Theorem anasss 460

Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)

Hypothesis

Ref	Expression
anasss.1	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
anasss	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Proof of Theorem anasss

Step	Hyp	Ref	Expression
1		anasss.1	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
2	1	exp31 412	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 411	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  anass  462  anabss3  665  f1elima  6775  fnfvof  7171  oecl  7884  oaass  7908  oen0  7933  oeworde  7940  omabs  7994  oiiniseg  8707  cardinfima  9233  fpwwe2lem12  9778  ltmul12a  11209  eluzp1m1  11992  lbzbi  12059  qreccl  12091  xrlttr  12259  elfzodifsumelfzo  12829  quoremnn0  12950  incexc2  14944  mertens  14991  ndvdsadd  15507  nn0seqcvgd  15656  isprm3  15768  isprm7  15791  pcval  15920  prdsval  16468  evlfcl  17215  frgpup1  18541  frgpup3lem  18543  ghmcmn  18590  gsumval3  18661  gsumzoppg  18697  ablfaclem2  18839  gsumdixp  18963  psrass1lem  19738  psrass1  19766  frlmgsum  20478  m2cpminvid2  20930  pmatcollpw2lem  20952  chcoeffeqlem  21060  neissex  21302  neiptopnei  21307  dissnlocfin  21703  tx1stc  21824  kqreglem1  21915  xpstopnlem1  21983  alexsublem  22218  metuel2  22740  icoopnst  23108  iocopnst  23109  volcn  23772  mbflimsup  23832  mbflim  23834  itg1addlem4  23865  itg1addlem5  23866  itg1climres  23880  limcflf  24044  dvcobr  24108  dvcnvlem  24138  dvfsumge  24184  mdegmullem  24237  plyeq0lem  24365  plypf1  24367  mtestbdd  24558  mbfulm  24559  fsumdvdscom  25324  muinv  25332  logfaclbnd  25360  logexprlim  25363  dchrinv  25399  lgsval3  25453  rpvmasum2  25614  dchrisum0lem1  25618  dchrisum0  25622  selberg  25650  selberg3lem1  25659  selberg34r  25673  pntsval2  25678  iscgrglt  25826  ercgrg  25829  legso  25911  oppperpex  26062  outpasch  26064  hpgerlem  26074  trgcopyeu  26115  dfcgra2  26138  inaghl  26149  colinearalg  26209  axeuclid  26262  axcontlem2  26264  axcontlem7  26269  wlkiswwlksupgr2  27176  grpoidinvlem4  27906  ipblnfi  28255  shmodsi  28792  eighmorth  29367  kbass5  29523  kbass6  29524  dmdmd  29703  atom1d  29756  mdsymlem2  29807  mdsymlem3  29808  mdsymlem4  29809  mdsymlem5  29810  fmptco1f1o  29972  fsumiunle  30111  2sqmo  30183  gsummpt2co  30314  suborng  30349  pstmxmet  30474  ordtconnlem1  30504  esumiun  30690  dya2iocnei  30878  omssubadd  30896  actfunsnf1o  31220  fsum2dsub  31223  reprsuc  31231  reprinfz1  31238  reprpmtf1o  31242  breprexplema  31246  circlemeth  31256  hgt750lemb  31272  resconn  31763  nosupbnd1lem5  32386  nocvxminlem  32421  uncf  33924  unccur  33928  fin2so  33932  matunitlindflem1  33942  poimirlem6  33952  poimirlem7  33953  poimirlem25  33971  poimirlem28  33974  poimirlem31  33977  poimirlem32  33978  broucube  33980  ismblfin  33987  mbfposadd  33993  itg2gt0cn  34001  ftc1anclem7  34027  ftc1anc  34029  cover2  34044  indexa  34064  filbcmb  34071  seqpo  34078  incsequz  34079  isbnd2  34117  ghomco  34225  unichnidl  34365  isfldidl  34402  dihvalc  37301  dihvalb  37305  radcnvrat  39346  reximddv3  40145  rexabslelem  40433  rexlimddv2  40837  dvnprodlem2  40950  etransclem46  41284  aacllem  43436