Theorem anasss 469

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  anass  471  anabss3  673  f1elima  7015  fnfvof  7417  oecl  8156  oaass  8181  oen0  8206  oeworde  8213  omabs  8268  oiiniseg  8991  cardinfima  9517  fpwwe2lem12  10057  ltmul12a  11490  eluzp1m1  12262  lbzbi  12330  qreccl  12362  xrlttr  12527  elfzodifsumelfzo  13097  quoremnn0  13218  incexc2  15187  mertens  15236  ndvdsadd  15755  nn0seqcvgd  15908  isprm3  16021  isprm7  16046  pcval  16175  prdsval  16722  evlfcl  17466  frgpup1  18895  frgpup3lem  18897  ghmcmn  18946  gsumval3  19021  gsumzoppg  19058  ablfaclem2  19202  gsumdixp  19353  psrass1lem  20151  psrass1  20179  frlmgsum  20910  m2cpminvid2  21357  pmatcollpw2lem  21379  chcoeffeqlem  21487  neissex  21729  neiptopnei  21734  dissnlocfin  22131  tx1stc  22252  kqreglem1  22343  xpstopnlem1  22411  alexsublem  22646  metuel2  23169  icoopnst  23537  iocopnst  23538  volcn  24201  mbflimsup  24261  mbflim  24263  itg1addlem4  24294  itg1addlem5  24295  itg1climres  24309  limcflf  24473  dvcobr  24537  dvcnvlem  24567  dvfsumge  24613  mdegmullem  24666  plyeq0lem  24794  plypf1  24796  mtestbdd  24987  mbfulm  24988  fsumdvdscom  25756  muinv  25764  logfaclbnd  25792  logexprlim  25795  dchrinv  25831  lgsval3  25885  2sqmo  26007  rpvmasum2  26082  dchrisum0lem1  26086  dchrisum0  26090  selberg  26118  selberg3lem1  26127  selberg34r  26141  pntsval2  26146  iscgrglt  26294  ercgrg  26297  legso  26379  oppperpex  26533  hpgerlem  26545  trgcopyeu  26586  dfcgra2  26610  inaghl  26625  colinearalg  26690  axeuclid  26743  axcontlem2  26745  axcontlem7  26750  wlkiswwlksupgr2  27649  grpoidinvlem4  28278  ipblnfi  28626  shmodsi  29160  eighmorth  29735  kbass5  29891  kbass6  29892  dmdmd  30071  atom1d  30124  mdsymlem2  30175  mdsymlem3  30176  mdsymlem4  30177  mdsymlem5  30178  fmptco1f1o  30372  fnpreimac  30410  fsumiunle  30540  s3f1  30618  swrdf1  30625  gsummpt2co  30681  tocyccntz  30781  cycpmconjs  30793  suborng  30883  eqgvscpbl  30914  prmidl2  30953  isprmidlc  30958  qsidomlem1  30960  qsidomlem2  30961  mxidlprm  30972  ssmxidllem  30973  lindsun  31016  lbsdiflsp0  31017  fedgmullem1  31020  fedgmul  31022  extdg1id  31048  pstmxmet  31132  ordtconnlem1  31162  esumiun  31348  dya2iocnei  31535  omssubadd  31553  actfunsnf1o  31870  fsum2dsub  31873  reprsuc  31881  reprinfz1  31888  reprpmtf1o  31892  breprexplema  31896  circlemeth  31906  hgt750lemb  31922  cusgr3cyclex  32378  resconn  32488  nosupbnd1lem5  33207  nocvxminlem  33242  pibt2  34692  uncf  34865  unccur  34869  fin2so  34873  matunitlindflem1  34882  poimirlem6  34892  poimirlem7  34893  poimirlem25  34911  poimirlem28  34914  poimirlem31  34917  poimirlem32  34918  broucube  34920  ismblfin  34927  mbfposadd  34933  itg2gt0cn  34941  ftc1anclem7  34967  ftc1anc  34969  cover2  34983  indexa  35002  filbcmb  35009  seqpo  35016  incsequz  35017  isbnd2  35055  ghomco  35163  unichnidl  35303  isfldidl  35340  dihvalc  38363  dihvalb  38367  radcnvrat  40639  reximddv3  41412  rexabslelem  41684  rexlimddv2  42096  dvnprodlem2  42224  etransclem46  42558  aacllem  44895