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  674  biadanid  822  rspc4v  3631  f1elima  7262  fnfvof  7687  frxp3  8137  oecl  8537  oaass  8561  oen0  8586  oeworde  8593  omabs  8650  oiiniseg  9528  cardinfima  10092  fpwwe2lem11  10636  ltmul12a  12070  eluzp1m1  12848  lbzbi  12920  qreccl  12953  xrlttr  13119  elfzodifsumelfzo  13698  quoremnn0  13821  incexc2  15784  mertens  15832  ndvdsadd  16353  nn0seqcvgd  16507  isprm3  16620  isprm7  16645  pcval  16777  prdsval  17401  evlfcl  18175  frgpup1  19643  frgpup3lem  19645  ghmcmn  19699  gsumval3  19775  gsumzoppg  19812  ablfaclem2  19956  gsumdixp  20131  frlmgsum  21327  psrass1lemOLD  21493  psrass1lem  21496  psrass1  21525  m2cpminvid2  22257  pmatcollpw2lem  22279  chcoeffeqlem  22387  neissex  22631  neiptopnei  22636  dissnlocfin  23033  tx1stc  23154  kqreglem1  23245  xpstopnlem1  23313  alexsublem  23548  metuel2  24074  icoopnst  24455  iocopnst  24456  volcn  25123  mbflimsup  25183  mbflim  25185  itg1addlem4  25216  itg1addlem4OLD  25217  itg1addlem5  25218  itg1climres  25232  limcflf  25398  dvcobr  25463  dvcnvlem  25493  dvfsumge  25539  mdegmullem  25596  plyeq0lem  25724  plypf1  25726  mtestbdd  25917  mbfulm  25918  fsumdvdscom  26689  muinv  26697  logfaclbnd  26725  logexprlim  26728  dchrinv  26764  lgsval3  26818  2sqmo  26940  rpvmasum2  27015  dchrisum0lem1  27019  dchrisum0  27023  selberg  27051  selberg3lem1  27060  selberg34r  27074  pntsval2  27079  nosupbnd1lem5  27215  noinfbnd1lem5  27230  nocvxminlem  27279  oldbday  27395  iscgrglt  27765  ercgrg  27768  legso  27850  oppperpex  28004  hpgerlem  28016  trgcopyeu  28057  dfcgra2  28081  inaghl  28096  colinearalg  28168  axeuclid  28221  axcontlem2  28223  axcontlem7  28228  wlkiswwlksupgr2  29131  grpoidinvlem4  29760  ipblnfi  30108  shmodsi  30642  eighmorth  31217  kbass5  31373  kbass6  31374  dmdmd  31553  atom1d  31606  mdsymlem2  31657  mdsymlem3  31658  mdsymlem4  31659  mdsymlem5  31660  fmptco1f1o  31857  2ndresdju  31874  fnpreimac  31896  fsumiunle  32035  s3f1  32113  swrdf1  32120  dfmgc2lem  32165  dfmgc2  32166  pwrssmgc  32170  mgcf1o  32173  gsummpt2co  32200  tocyccntz  32303  cycpmconjs  32315  urpropd  32378  isdrng4  32395  suborng  32433  eqgvscpbl  32465  dvdsruasso  32490  nsgmgclem  32522  nsgmgc  32523  nsgqusf1olem2  32525  nsgqusf1olem3  32526  ghmquskerlem3  32531  lmhmqusker  32534  intlidl  32536  rhmpreimaidl  32537  rhmquskerlem  32543  elrspunidl  32546  elrspunsn  32547  idlinsubrg  32549  rhmimaidl  32550  drngidl  32551  prmidl2  32559  idlmulssprm  32560  isprmidlc  32566  rhmpreimaprmidl  32570  qsidomlem1  32571  qsidomlem2  32572  mxidlprm  32586  mxidlirredi  32587  ssmxidllem  32589  opprlidlabs  32599  qsdrngi  32609  ply1degltdimlem  32707  ply1degltdim  32708  lindsun  32710  lbsdiflsp0  32711  fedgmullem1  32714  fedgmul  32716  extdg1id  32742  evls1maplmhm  32760  minplyirred  32770  zart0  32859  pstmxmet  32877  ordtconnlem1  32904  esumiun  33092  dya2iocnei  33281  omssubadd  33299  actfunsnf1o  33616  fsum2dsub  33619  reprsuc  33627  reprinfz1  33634  reprpmtf1o  33638  breprexplema  33642  circlemeth  33652  hgt750lemb  33668  cusgr3cyclex  34127  resconn  34237  gg-dvcobr  35176  pibt2  36298  uncf  36467  unccur  36471  fin2so  36475  matunitlindflem1  36484  poimirlem6  36494  poimirlem7  36495  poimirlem25  36513  poimirlem28  36516  poimirlem31  36519  poimirlem32  36520  broucube  36522  ismblfin  36529  mbfposadd  36535  itg2gt0cn  36543  ftc1anclem7  36567  ftc1anc  36569  cover2  36583  indexa  36601  filbcmb  36608  seqpo  36615  incsequz  36616  isbnd2  36651  ghomco  36759  unichnidl  36899  isfldidl  36936  dihvalc  40104  dihvalb  40108  uzindd  40842  aks4d1p8  40952  evlselv  41159  fsuppind  41162  radcnvrat  43073  reximddv3  43840  rexabslelem  44128  rexlimddv2  44539  dvnprodlem2  44663  etransclem46  44996  lubeldm2  47589  glbeldm2  47590  aacllem  47848