Theorem anasss 677

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 628	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 448	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  anass  679  anabss3  860  f1elima  6421  fnfvof  6809  oecl  7504  oaass  7528  oen0  7553  oeworde  7560  omabs  7614  oiiniseg  8321  cardinfima  8803  fpwwe2lem12  9342  ltmul12a  10758  eluzp1m1  11587  lbzbi  11652  qreccl  11684  xrlttr  11849  elfzodifsumelfzo  12401  quoremnn0  12517  incexc2  14409  mertens  14457  ndvdsadd  14972  nn0seqcvgd  15121  isprm3  15234  isprm7  15258  pcval  15387  prdsval  15938  evlfcl  16685  frgpup1  18011  frgpup3lem  18013  ghmcmn  18060  gsumval3  18131  gsumzoppg  18167  ablfaclem2  18308  gsumdixp  18432  psrass1lem  19198  psrass1  19226  frlmgsum  19930  m2cpminvid2  20379  pmatcollpw2lem  20401  chcoeffeqlem  20509  neissex  20741  neiptopnei  20746  dissnlocfin  21142  tx1stc  21263  kqreglem1  21354  xpstopnlem1  21422  alexsublem  21658  metuel2  22180  icoopnst  22546  iocopnst  22547  volcn  23180  mbflimsup  23239  mbflim  23241  itg1addlem4  23272  itg1addlem5  23273  itg1climres  23287  limcflf  23451  dvcobr  23515  dvcnvlem  23543  dvfsumge  23589  mdegmullem  23642  plyeq0lem  23770  plypf1  23772  mtestbdd  23963  mbfulm  23964  fsumdvdscom  24711  muinv  24719  logfaclbnd  24747  logexprlim  24750  dchrinv  24786  lgsval3  24840  rpvmasum2  25001  dchrisum0lem1  25005  dchrisum0  25009  selberg  25037  selberg3lem1  25046  selberg34r  25060  pntsval2  25065  iscgrglt  25209  ercgrg  25212  legso  25294  oppperpex  25445  outpasch  25447  hpgerlem  25457  trgcopyeu  25498  dfcgra2  25521  inaghl  25531  colinearalg  25590  axeuclid  25643  axcontlem2  25645  axcontlem7  25650  grpoidinvlem4  26745  ipblnfi  27095  shmodsi  27632  eighmorth  28207  kbass5  28363  kbass6  28364  dmdmd  28543  atom1d  28596  mdsymlem2  28647  mdsymlem3  28648  mdsymlem4  28649  mdsymlem5  28650  2sqmo  28980  gsummpt2co  29111  suborng  29146  pstmxmet  29268  ordtconlem1  29298  esumiun  29483  dya2iocnei  29671  omssubadd  29689  rescon  30482  nocvxminlem  31089  nobndlem6  31096  uncf  32558  unccur  32562  fin2so  32566  matunitlindflem1  32575  poimirlem6  32585  poimirlem7  32586  poimirlem25  32604  poimirlem28  32607  poimirlem31  32610  poimirlem32  32611  broucube  32613  ismblfin  32620  mbfposadd  32627  itg2gt0cn  32635  ftc1anclem7  32661  ftc1anc  32663  cover2  32678  indexa  32698  filbcmb  32705  seqpo  32713  incsequz  32714  isbnd2  32752  ghomco  32860  unichnidl  33000  isfldidl  33037  dihvalc  35540  dihvalb  35544  radcnvrat  37535  dvnprodlem2  38837  etransclem46  39173  1wlkiswwlksupgr2  41074  aacllem  42356