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  675  biadanid  822  reximddv3  3146  rspc4v  3599  f1elima  7204  fnfvof  7634  frxp3  8091  oecl  8462  oaass  8486  oen0  8511  oeworde  8518  omabs  8576  oiiniseg  9444  cardinfima  10010  fpwwe2lem11  10554  ltmul12a  11998  eluzp1m1  12779  lbzbi  12855  qreccl  12888  xrlttr  13060  elfzodifsumelfzo  13652  quoremnn0  13778  incexc2  15763  mertens  15811  ndvdsadd  16339  nn0seqcvgd  16499  isprm3  16612  isprm7  16637  pcval  16774  prdsval  17377  evlfcl  18146  ghmqusnsg  19179  ghmquskerlem3  19183  frgpup1  19672  frgpup3lem  19674  ghmcmn  19728  gsumval3  19804  gsumzoppg  19841  ablfaclem2  19985  gsumdixp  20222  suborng  20779  rhmpreimaidl  21202  rhmqusnsg  21210  frlmgsum  21697  psrass1lem  21857  psrass1  21889  psdmul  22069  evls1maplmhm  22280  m2cpminvid2  22658  pmatcollpw2lem  22680  chcoeffeqlem  22788  neissex  23030  neiptopnei  23035  dissnlocfin  23432  tx1stc  23553  kqreglem1  23644  xpstopnlem1  23712  alexsublem  23947  metuel2  24469  icoopnst  24852  iocopnst  24853  volcn  25523  mbflimsup  25583  mbflim  25585  itg1addlem4  25616  itg1addlem5  25617  itg1climres  25631  limcflf  25798  dvcobr  25865  dvcobrOLD  25866  dvcnvlem  25896  dvfsumge  25944  mdegmullem  25999  plyeq0lem  26131  plypf1  26133  mtestbdd  26330  mbfulm  26331  fsumdvdscom  27111  muinv  27119  logfaclbnd  27149  logexprlim  27152  dchrinv  27188  lgsval3  27242  2sqmo  27364  rpvmasum2  27439  dchrisum0lem1  27443  dchrisum0  27447  selberg  27475  selberg3lem1  27484  selberg34r  27498  pntsval2  27503  nosupbnd1lem5  27640  noinfbnd1lem5  27655  nocvxminlem  27706  oldbday  27833  peano5uzs  28315  iscgrglt  28477  ercgrg  28480  legso  28562  oppperpex  28716  hpgerlem  28728  trgcopyeu  28769  dfcgra2  28793  inaghl  28808  colinearalg  28873  axeuclid  28926  axcontlem2  28928  axcontlem7  28933  wlkiswwlksupgr2  29840  grpoidinvlem4  30469  ipblnfi  30817  shmodsi  31351  eighmorth  31926  kbass5  32082  kbass6  32083  dmdmd  32262  atom1d  32315  mdsymlem2  32366  mdsymlem3  32367  mdsymlem4  32368  mdsymlem5  32369  fmptco1f1o  32590  2ndresdju  32606  fnpreimac  32628  fsumiunle  32787  s3f1  32901  swrdf1  32911  dfmgc2lem  32950  dfmgc2  32951  pwrssmgc  32955  mgcf1o  32958  chnso  32969  mndlrinvb  32992  mndlactf1  32993  mndractf1  32995  gsummpt2co  33014  gsumwrd2dccatlem  33032  tocyccntz  33099  cycpmconjs  33111  conjga  33125  fxpsubrg  33129  urpropd  33185  elrgspnlem2  33196  elrgspnlem4  33198  elrgspnsubrunlem2  33201  elrgspnsubrun  33202  erler  33218  rlocaddval  33221  rlocmulval  33222  rlocf1  33226  domnprodn0  33228  rrgsubm  33236  subrdom  33237  isdrng4  33247  eqgvscpbl  33300  dvdsruasso  33335  nsgmgclem  33361  nsgmgc  33362  nsgqusf1olem2  33364  nsgqusf1olem3  33365  lmhmqusker  33367  intlidl  33370  rhmquskerlem  33375  elrspunidl  33378  elrspunsn  33379  idlinsubrg  33381  rhmimaidl  33382  drngidl  33383  prmidl2  33391  idlmulssprm  33392  isprmidlc  33397  rhmpreimaprmidl  33401  qsidomlem1  33402  qsidomlem2  33403  ssdifidllem  33406  ssdifidlprm  33408  mxidlprm  33420  mxidlirredi  33421  ssmxidllem  33423  opprlidlabs  33435  qsdrngi  33445  rsprprmprmidl  33472  rsprprmprmidlb  33473  rprmirred  33481  rprmirredb  33482  rprmdvdsprod  33484  1arithidom  33487  1arithufdlem3  33496  1arithufdlem4  33497  r1plmhm  33554  r1pquslmic  33555  ply1degltdimlem  33597  ply1degltdim  33598  lindsun  33600  lbsdiflsp0  33601  fedgmullem1  33604  fedgmul  33606  lactlmhm  33609  assalactf1o  33610  extdg1id  33640  fldextrspunlsplem  33647  fldextrspunlsp  33648  minplyirred  33680  algextdeglem8  33693  constrextdg2lem  33717  constrextdg2  33718  constrfiss  33720  constrsdrg  33744  cos9thpiminplylem2  33752  zart0  33848  pstmxmet  33866  ordtconnlem1  33893  esumiun  34063  dya2iocnei  34252  omssubadd  34270  actfunsnf1o  34574  fsum2dsub  34577  reprsuc  34585  reprinfz1  34592  reprpmtf1o  34596  breprexplema  34600  circlemeth  34610  hgt750lemb  34626  cusgr3cyclex  35111  resconn  35221  pibt2  37393  uncf  37581  unccur  37585  fin2so  37589  matunitlindflem1  37598  poimirlem6  37608  poimirlem7  37609  poimirlem25  37627  poimirlem28  37630  poimirlem31  37633  poimirlem32  37634  broucube  37636  ismblfin  37643  mbfposadd  37649  itg2gt0cn  37657  ftc1anclem7  37681  ftc1anc  37683  cover2  37697  indexa  37715  filbcmb  37722  seqpo  37729  incsequz  37730  isbnd2  37765  ghomco  37873  unichnidl  38013  isfldidl  38050  dihvalc  41215  dihvalb  41219  uzindd  41953  aks4d1p8  42063  evlselv  42563  fsuppind  42566  radcnvrat  44290  rexabslelem  45401  rexlimddv2  45808  dvnprodlem2  45932  etransclem46  46265  isgrtri  47931  grlimgrtri  47991  lubeldm2  48944  glbeldm2  48945  thincciso2  49444  aacllem  49790