Theorem anasss 679

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

Syntax hints:   → wi 4   ∧ wa 384

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 197  df-an 386

This theorem is referenced by:  anass  681  anabss3  864  f1elima  6520  fnfvof  6911  oecl  7617  oaass  7641  oen0  7666  oeworde  7673  omabs  7727  oiiniseg  8438  cardinfima  8920  fpwwe2lem12  9463  ltmul12a  10879  eluzp1m1  11711  lbzbi  11776  qreccl  11808  xrlttr  11973  elfzodifsumelfzo  12533  quoremnn0  12655  incexc2  14570  mertens  14618  ndvdsadd  15134  nn0seqcvgd  15283  isprm3  15396  isprm7  15420  pcval  15549  prdsval  16115  evlfcl  16862  frgpup1  18188  frgpup3lem  18190  ghmcmn  18237  gsumval3  18308  gsumzoppg  18344  ablfaclem2  18485  gsumdixp  18609  psrass1lem  19377  psrass1  19405  frlmgsum  20111  m2cpminvid2  20560  pmatcollpw2lem  20582  chcoeffeqlem  20690  neissex  20931  neiptopnei  20936  dissnlocfin  21332  tx1stc  21453  kqreglem1  21544  xpstopnlem1  21612  alexsublem  21848  metuel2  22370  icoopnst  22738  iocopnst  22739  volcn  23374  mbflimsup  23433  mbflim  23435  itg1addlem4  23466  itg1addlem5  23467  itg1climres  23481  limcflf  23645  dvcobr  23709  dvcnvlem  23739  dvfsumge  23785  mdegmullem  23838  plyeq0lem  23966  plypf1  23968  mtestbdd  24159  mbfulm  24160  fsumdvdscom  24911  muinv  24919  logfaclbnd  24947  logexprlim  24950  dchrinv  24986  lgsval3  25040  rpvmasum2  25201  dchrisum0lem1  25205  dchrisum0  25209  selberg  25237  selberg3lem1  25246  selberg34r  25260  pntsval2  25265  iscgrglt  25409  ercgrg  25412  legso  25494  oppperpex  25645  outpasch  25647  hpgerlem  25657  trgcopyeu  25698  dfcgra2  25721  inaghl  25731  colinearalg  25790  axeuclid  25843  axcontlem2  25845  axcontlem7  25850  wlkiswwlksupgr2  26763  grpoidinvlem4  27361  ipblnfi  27711  shmodsi  28248  eighmorth  28823  kbass5  28979  kbass6  28980  dmdmd  29159  atom1d  29212  mdsymlem2  29263  mdsymlem3  29264  mdsymlem4  29265  mdsymlem5  29266  fmptco1f1o  29434  fsumiunle  29575  2sqmo  29649  gsummpt2co  29780  suborng  29815  pstmxmet  29940  ordtconnlem1  29970  esumiun  30156  dya2iocnei  30344  omssubadd  30362  actfunsnf1o  30682  fsum2dsub  30685  reprsuc  30693  reprinfz1  30700  reprpmtf1o  30704  breprexplema  30708  circlemeth  30718  hgt750lemb  30734  resconn  31228  nosupbnd1lem5  31858  nocvxminlem  31893  uncf  33388  unccur  33392  fin2so  33396  matunitlindflem1  33405  poimirlem6  33415  poimirlem7  33416  poimirlem25  33434  poimirlem28  33437  poimirlem31  33440  poimirlem32  33441  broucube  33443  ismblfin  33450  mbfposadd  33457  itg2gt0cn  33465  ftc1anclem7  33491  ftc1anc  33493  cover2  33508  indexa  33528  filbcmb  33535  seqpo  33543  incsequz  33544  isbnd2  33582  ghomco  33690  unichnidl  33830  isfldidl  33867  dihvalc  36522  dihvalb  36526  radcnvrat  38513  reximddv3  39343  rexabslelem  39645  rexlimddv2  40049  dvnprodlem2  40162  etransclem46  40497  aacllem  42547