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  676  biadanid  823  reximddv3  3155  rspc4v  3598  f1elima  7219  fnfvof  7649  frxp3  8103  oecl  8474  oaass  8498  oen0  8524  oeworde  8531  omabs  8589  oiiniseg  9450  cardinfima  10019  fpwwe2lem11  10564  ltmul12a  12009  eluzp1m1  12789  lbzbi  12861  qreccl  12894  xrlttr  13066  elfzodifsumelfzo  13659  quoremnn0  13788  incexc2  15773  mertens  15821  ndvdsadd  16349  nn0seqcvgd  16509  isprm3  16622  isprm7  16647  pcval  16784  prdsval  17387  evlfcl  18157  chnso  18559  ghmqusnsg  19223  ghmquskerlem3  19227  frgpup1  19716  frgpup3lem  19718  ghmcmn  19772  gsumval3  19848  gsumzoppg  19885  ablfaclem2  20029  gsumdixp  20266  suborng  20821  rhmpreimaidl  21244  rhmqusnsg  21252  frlmgsum  21739  psrass1lem  21900  psrass1  21931  psdmul  22121  evls1maplmhm  22333  m2cpminvid2  22711  pmatcollpw2lem  22733  chcoeffeqlem  22841  neissex  23083  neiptopnei  23088  dissnlocfin  23485  tx1stc  23606  kqreglem1  23697  xpstopnlem1  23765  alexsublem  24000  metuel2  24521  icoopnst  24904  iocopnst  24905  volcn  25575  mbflimsup  25635  mbflim  25637  itg1addlem4  25668  itg1addlem5  25669  itg1climres  25683  limcflf  25850  dvcobr  25917  dvcobrOLD  25918  dvcnvlem  25948  dvfsumge  25996  mdegmullem  26051  plyeq0lem  26183  plypf1  26185  mtestbdd  26382  mbfulm  26383  fsumdvdscom  27163  muinv  27171  logfaclbnd  27201  logexprlim  27204  dchrinv  27240  lgsval3  27294  2sqmo  27416  rpvmasum2  27491  dchrisum0lem1  27495  dchrisum0  27499  selberg  27527  selberg3lem1  27536  selberg34r  27550  pntsval2  27555  nosupbnd1lem5  27692  noinfbnd1lem5  27707  nocvxminlem  27762  oldbday  27909  peano5uzs  28412  iscgrglt  28598  ercgrg  28601  legso  28683  oppperpex  28837  hpgerlem  28849  trgcopyeu  28890  dfcgra2  28914  inaghl  28929  colinearalg  28995  axeuclid  29048  axcontlem2  29050  axcontlem7  29055  wlkiswwlksupgr2  29962  grpoidinvlem4  30594  ipblnfi  30942  shmodsi  31476  eighmorth  32051  kbass5  32207  kbass6  32208  dmdmd  32387  atom1d  32440  mdsymlem2  32491  mdsymlem3  32492  mdsymlem4  32493  mdsymlem5  32494  fmptco1f1o  32722  2ndresdju  32738  fnpreimac  32759  fsumiunle  32920  s3f1  33039  swrdf1  33048  dfmgc2lem  33087  dfmgc2  33088  pwrssmgc  33092  mgcf1o  33095  mndlrinvb  33117  mndlactf1  33118  mndractf1  33120  gsummpt2co  33141  gsumwrd2dccatlem  33170  tocyccntz  33237  cycpmconjs  33249  conjga  33263  fxpsubrg  33267  urpropd  33324  elrgspnlem2  33336  elrgspnlem4  33338  elrgspnsubrunlem2  33341  elrgspnsubrun  33342  erler  33358  rlocaddval  33361  rlocmulval  33362  rlocf1  33366  domnprodn0  33368  domnprodeq0  33369  rrgsubm  33377  subrdom  33378  isdrng4  33388  eqgvscpbl  33442  dvdsruasso  33477  nsgmgclem  33503  nsgmgc  33504  nsgqusf1olem2  33506  nsgqusf1olem3  33507  lmhmqusker  33509  intlidl  33512  rhmquskerlem  33517  elrspunidl  33520  elrspunsn  33521  idlinsubrg  33523  rhmimaidl  33524  drngidl  33525  prmidl2  33533  idlmulssprm  33534  isprmidlc  33539  rhmpreimaprmidl  33543  qsidomlem1  33544  qsidomlem2  33545  ssdifidllem  33548  ssdifidlprm  33550  mxidlprm  33562  mxidlirredi  33563  ssmxidllem  33565  opprlidlabs  33577  qsdrngi  33587  rsprprmprmidl  33614  rsprprmprmidlb  33615  rprmirred  33623  rprmirredb  33624  rprmdvdsprod  33626  1arithidom  33629  1arithufdlem3  33638  1arithufdlem4  33639  deg1prod  33675  r1plmhm  33702  r1pquslmic  33703  extvfvcl  33712  mplvrpmga  33721  mplvrpmmhm  33722  mplvrpmrhm  33723  psrgsum  33724  psrmonprod  33728  esplyfval1  33749  esplyfvaln  33750  vieta  33756  ply1degltdimlem  33799  ply1degltdim  33800  lindsun  33802  lbsdiflsp0  33803  fedgmullem1  33806  fedgmul  33808  lactlmhm  33811  assalactf1o  33812  extdg1id  33843  fldextrspunlsplem  33850  fldextrspunlsp  33851  extdgfialglem2  33870  extdgfialg  33871  minplyirred  33888  algextdeglem8  33901  constrextdg2lem  33925  constrextdg2  33926  constrfiss  33928  constrsdrg  33952  cos9thpiminplylem2  33960  zart0  34056  pstmxmet  34074  ordtconnlem1  34101  esumiun  34271  dya2iocnei  34459  omssubadd  34477  actfunsnf1o  34781  fsum2dsub  34784  reprsuc  34792  reprinfz1  34799  reprpmtf1o  34803  breprexplema  34807  circlemeth  34817  hgt750lemb  34833  cusgr3cyclex  35349  resconn  35459  pibt2  37669  uncf  37847  unccur  37851  fin2so  37855  matunitlindflem1  37864  poimirlem6  37874  poimirlem7  37875  poimirlem25  37893  poimirlem28  37896  poimirlem31  37899  poimirlem32  37900  broucube  37902  ismblfin  37909  mbfposadd  37915  itg2gt0cn  37923  ftc1anclem7  37947  ftc1anc  37949  cover2  37963  indexa  37981  filbcmb  37988  seqpo  37995  incsequz  37996  isbnd2  38031  ghomco  38139  unichnidl  38279  isfldidl  38316  dihvalc  41606  dihvalb  41610  uzindd  42344  aks4d1p8  42454  evlselv  42942  fsuppind  42945  radcnvrat  44667  rexabslelem  45773  rexlimddv2  46178  dvnprodlem2  46302  etransclem46  46635  isgrtri  48300  grlimgrtri  48360  lubeldm2  49312  glbeldm2  49313  thincciso2  49811  aacllem  50157