Theorem anasss 468

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  anass  470  anabss3  673  biadanid  821  f1elima  7168  fnfvof  7582  oecl  8398  oaass  8423  oen0  8448  oeworde  8455  omabs  8512  oiiniseg  9336  cardinfima  9899  fpwwe2lem11  10443  ltmul12a  11877  eluzp1m1  12654  lbzbi  12722  qreccl  12755  xrlttr  12920  elfzodifsumelfzo  13499  quoremnn0  13622  incexc2  15595  mertens  15643  ndvdsadd  16164  nn0seqcvgd  16320  isprm3  16433  isprm7  16458  pcval  16590  prdsval  17211  evlfcl  17985  frgpup1  19426  frgpup3lem  19428  ghmcmn  19478  gsumval3  19553  gsumzoppg  19590  ablfaclem2  19734  gsumdixp  19893  frlmgsum  21024  psrass1lemOLD  21188  psrass1lem  21191  psrass1  21219  m2cpminvid2  21949  pmatcollpw2lem  21971  chcoeffeqlem  22079  neissex  22323  neiptopnei  22328  dissnlocfin  22725  tx1stc  22846  kqreglem1  22937  xpstopnlem1  23005  alexsublem  23240  metuel2  23766  icoopnst  24147  iocopnst  24148  volcn  24815  mbflimsup  24875  mbflim  24877  itg1addlem4  24908  itg1addlem4OLD  24909  itg1addlem5  24910  itg1climres  24924  limcflf  25090  dvcobr  25155  dvcnvlem  25185  dvfsumge  25231  mdegmullem  25288  plyeq0lem  25416  plypf1  25418  mtestbdd  25609  mbfulm  25610  fsumdvdscom  26379  muinv  26387  logfaclbnd  26415  logexprlim  26418  dchrinv  26454  lgsval3  26508  2sqmo  26630  rpvmasum2  26705  dchrisum0lem1  26709  dchrisum0  26713  selberg  26741  selberg3lem1  26750  selberg34r  26764  pntsval2  26769  iscgrglt  26920  ercgrg  26923  legso  27005  oppperpex  27159  hpgerlem  27171  trgcopyeu  27212  dfcgra2  27236  inaghl  27251  colinearalg  27323  axeuclid  27376  axcontlem2  27378  axcontlem7  27383  wlkiswwlksupgr2  28287  grpoidinvlem4  28914  ipblnfi  29262  shmodsi  29796  eighmorth  30371  kbass5  30527  kbass6  30528  dmdmd  30707  atom1d  30760  mdsymlem2  30811  mdsymlem3  30812  mdsymlem4  30813  mdsymlem5  30814  fmptco1f1o  31013  2ndresdju  31031  fnpreimac  31053  fsumiunle  31188  s3f1  31266  swrdf1  31273  dfmgc2lem  31318  dfmgc2  31319  pwrssmgc  31323  mgcf1o  31326  gsummpt2co  31353  tocyccntz  31456  cycpmconjs  31468  suborng  31559  eqgvscpbl  31595  nsgmgclem  31641  nsgmgc  31642  nsgqusf1olem2  31644  nsgqusf1olem3  31645  intlidl  31647  rhmpreimaidl  31648  elrspunidl  31651  idlinsubrg  31653  rhmimaidl  31654  prmidl2  31661  idlmulssprm  31662  isprmidlc  31668  rhmpreimaprmidl  31672  qsidomlem1  31673  qsidomlem2  31674  mxidlprm  31685  ssmxidllem  31686  lindsun  31751  lbsdiflsp0  31752  fedgmullem1  31755  fedgmul  31757  extdg1id  31783  zart0  31874  pstmxmet  31892  ordtconnlem1  31919  esumiun  32107  dya2iocnei  32294  omssubadd  32312  actfunsnf1o  32629  fsum2dsub  32632  reprsuc  32640  reprinfz1  32647  reprpmtf1o  32651  breprexplema  32655  circlemeth  32665  hgt750lemb  32681  cusgr3cyclex  33143  resconn  33253  nosupbnd1lem5  33960  noinfbnd1lem5  33975  nocvxminlem  34017  oldbday  34126  pibt2  35632  uncf  35800  unccur  35804  fin2so  35808  matunitlindflem1  35817  poimirlem6  35827  poimirlem7  35828  poimirlem25  35846  poimirlem28  35849  poimirlem31  35852  poimirlem32  35853  broucube  35855  ismblfin  35862  mbfposadd  35868  itg2gt0cn  35876  ftc1anclem7  35900  ftc1anc  35902  cover2  35916  indexa  35935  filbcmb  35942  seqpo  35949  incsequz  35950  isbnd2  35985  ghomco  36093  unichnidl  36233  isfldidl  36270  dihvalc  39289  dihvalb  39293  uzindd  40027  aks4d1p8  40137  fsuppind  40316  radcnvrat  41970  reximddv3  42738  rexabslelem  43006  rexlimddv2  43413  dvnprodlem2  43537  etransclem46  43870  lubeldm2  46308  glbeldm2  46309  aacllem  46563