Theorem anasss 466

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  anass  468  anabss3  674  biadanid  822  reximddv3  3178  rspc4v  3655  f1elima  7300  fnfvof  7731  frxp3  8192  oecl  8593  oaass  8617  oen0  8642  oeworde  8649  omabs  8707  oiiniseg  9602  cardinfima  10166  fpwwe2lem11  10710  ltmul12a  12150  eluzp1m1  12929  lbzbi  13001  qreccl  13034  xrlttr  13202  elfzodifsumelfzo  13782  quoremnn0  13907  incexc2  15886  mertens  15934  ndvdsadd  16458  nn0seqcvgd  16617  isprm3  16730  isprm7  16755  pcval  16891  prdsval  17515  evlfcl  18292  ghmqusnsg  19322  ghmquskerlem3  19326  frgpup1  19817  frgpup3lem  19819  ghmcmn  19873  gsumval3  19949  gsumzoppg  19986  ablfaclem2  20130  gsumdixp  20342  rhmpreimaidl  21310  rhmqusnsg  21318  frlmgsum  21815  psrass1lem  21975  psrass1  22007  psdmul  22193  evls1maplmhm  22402  m2cpminvid2  22782  pmatcollpw2lem  22804  chcoeffeqlem  22912  neissex  23156  neiptopnei  23161  dissnlocfin  23558  tx1stc  23679  kqreglem1  23770  xpstopnlem1  23838  alexsublem  24073  metuel2  24599  icoopnst  24988  iocopnst  24989  volcn  25660  mbflimsup  25720  mbflim  25722  itg1addlem4  25753  itg1addlem4OLD  25754  itg1addlem5  25755  itg1climres  25769  limcflf  25936  dvcobr  26003  dvcobrOLD  26004  dvcnvlem  26034  dvfsumge  26082  mdegmullem  26137  plyeq0lem  26269  plypf1  26271  mtestbdd  26466  mbfulm  26467  fsumdvdscom  27246  muinv  27254  logfaclbnd  27284  logexprlim  27287  dchrinv  27323  lgsval3  27377  2sqmo  27499  rpvmasum2  27574  dchrisum0lem1  27578  dchrisum0  27582  selberg  27610  selberg3lem1  27619  selberg34r  27633  pntsval2  27638  nosupbnd1lem5  27775  noinfbnd1lem5  27790  nocvxminlem  27840  oldbday  27957  peano5uzs  28408  iscgrglt  28540  ercgrg  28543  legso  28625  oppperpex  28779  hpgerlem  28791  trgcopyeu  28832  dfcgra2  28856  inaghl  28871  colinearalg  28943  axeuclid  28996  axcontlem2  28998  axcontlem7  29003  wlkiswwlksupgr2  29910  grpoidinvlem4  30539  ipblnfi  30887  shmodsi  31421  eighmorth  31996  kbass5  32152  kbass6  32153  dmdmd  32332  atom1d  32385  mdsymlem2  32436  mdsymlem3  32437  mdsymlem4  32438  mdsymlem5  32439  fmptco1f1o  32652  2ndresdju  32667  fnpreimac  32689  fsumiunle  32833  s3f1  32913  swrdf1  32923  dfmgc2lem  32968  dfmgc2  32969  pwrssmgc  32973  mgcf1o  32976  chnso  32986  mndlrinvb  33011  mndlactf1  33012  mndractf1  33014  gsummpt2co  33031  tocyccntz  33137  cycpmconjs  33149  urpropd  33212  erler  33237  rlocaddval  33240  rlocmulval  33241  rlocf1  33245  domnprodn0  33247  rrgsubm  33253  subrdom  33254  isdrng4  33264  suborng  33310  eqgvscpbl  33343  dvdsruasso  33378  nsgmgclem  33404  nsgmgc  33405  nsgqusf1olem2  33407  nsgqusf1olem3  33408  lmhmqusker  33410  intlidl  33413  rhmquskerlem  33418  elrspunidl  33421  elrspunsn  33422  idlinsubrg  33424  rhmimaidl  33425  drngidl  33426  prmidl2  33434  idlmulssprm  33435  isprmidlc  33440  rhmpreimaprmidl  33444  qsidomlem1  33445  qsidomlem2  33446  ssdifidllem  33449  ssdifidlprm  33451  mxidlprm  33463  mxidlirredi  33464  ssmxidllem  33466  opprlidlabs  33478  qsdrngi  33488  rsprprmprmidl  33515  rsprprmprmidlb  33516  rprmirred  33524  rprmirredb  33525  rprmdvdsprod  33527  1arithidom  33530  1arithufdlem3  33539  1arithufdlem4  33540  r1plmhm  33595  r1pquslmic  33596  ply1degltdimlem  33635  ply1degltdim  33636  lindsun  33638  lbsdiflsp0  33639  fedgmullem1  33642  fedgmul  33644  lactlmhm  33647  assalactf1o  33648  extdg1id  33676  minplyirred  33704  algextdeglem8  33715  zart0  33825  pstmxmet  33843  ordtconnlem1  33870  esumiun  34058  dya2iocnei  34247  omssubadd  34265  actfunsnf1o  34581  fsum2dsub  34584  reprsuc  34592  reprinfz1  34599  reprpmtf1o  34603  breprexplema  34607  circlemeth  34617  hgt750lemb  34633  cusgr3cyclex  35104  resconn  35214  pibt2  37383  uncf  37559  unccur  37563  fin2so  37567  matunitlindflem1  37576  poimirlem6  37586  poimirlem7  37587  poimirlem25  37605  poimirlem28  37608  poimirlem31  37611  poimirlem32  37612  broucube  37614  ismblfin  37621  mbfposadd  37627  itg2gt0cn  37635  ftc1anclem7  37659  ftc1anc  37661  cover2  37675  indexa  37693  filbcmb  37700  seqpo  37707  incsequz  37708  isbnd2  37743  ghomco  37851  unichnidl  37991  isfldidl  38028  dihvalc  41190  dihvalb  41194  uzindd  41933  aks4d1p8  42044  evlselv  42542  fsuppind  42545  radcnvrat  44283  rexabslelem  45333  rexlimddv2  45744  dvnprodlem2  45868  etransclem46  46201  isgrtri  47794  grlimgrtri  47820  lubeldm2  48636  glbeldm2  48637  aacllem  48895