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  3150  rspc4v  3608  f1elima  7238  fnfvof  7670  frxp3  8130  oecl  8501  oaass  8525  oen0  8550  oeworde  8557  omabs  8615  oiiniseg  9486  cardinfima  10050  fpwwe2lem11  10594  ltmul12a  12038  eluzp1m1  12819  lbzbi  12895  qreccl  12928  xrlttr  13100  elfzodifsumelfzo  13692  quoremnn0  13818  incexc2  15804  mertens  15852  ndvdsadd  16380  nn0seqcvgd  16540  isprm3  16653  isprm7  16678  pcval  16815  prdsval  17418  evlfcl  18183  ghmqusnsg  19214  ghmquskerlem3  19218  frgpup1  19705  frgpup3lem  19707  ghmcmn  19761  gsumval3  19837  gsumzoppg  19874  ablfaclem2  20018  gsumdixp  20228  rhmpreimaidl  21187  rhmqusnsg  21195  frlmgsum  21681  psrass1lem  21841  psrass1  21873  psdmul  22053  evls1maplmhm  22264  m2cpminvid2  22642  pmatcollpw2lem  22664  chcoeffeqlem  22772  neissex  23014  neiptopnei  23019  dissnlocfin  23416  tx1stc  23537  kqreglem1  23628  xpstopnlem1  23696  alexsublem  23931  metuel2  24453  icoopnst  24836  iocopnst  24837  volcn  25507  mbflimsup  25567  mbflim  25569  itg1addlem4  25600  itg1addlem5  25601  itg1climres  25615  limcflf  25782  dvcobr  25849  dvcobrOLD  25850  dvcnvlem  25880  dvfsumge  25928  mdegmullem  25983  plyeq0lem  26115  plypf1  26117  mtestbdd  26314  mbfulm  26315  fsumdvdscom  27095  muinv  27103  logfaclbnd  27133  logexprlim  27136  dchrinv  27172  lgsval3  27226  2sqmo  27348  rpvmasum2  27423  dchrisum0lem1  27427  dchrisum0  27431  selberg  27459  selberg3lem1  27468  selberg34r  27482  pntsval2  27487  nosupbnd1lem5  27624  noinfbnd1lem5  27639  nocvxminlem  27689  oldbday  27812  peano5uzs  28292  iscgrglt  28441  ercgrg  28444  legso  28526  oppperpex  28680  hpgerlem  28692  trgcopyeu  28733  dfcgra2  28757  inaghl  28772  colinearalg  28837  axeuclid  28890  axcontlem2  28892  axcontlem7  28897  wlkiswwlksupgr2  29807  grpoidinvlem4  30436  ipblnfi  30784  shmodsi  31318  eighmorth  31893  kbass5  32049  kbass6  32050  dmdmd  32229  atom1d  32282  mdsymlem2  32333  mdsymlem3  32334  mdsymlem4  32335  mdsymlem5  32336  fmptco1f1o  32557  2ndresdju  32573  fnpreimac  32595  fsumiunle  32754  s3f1  32868  swrdf1  32878  dfmgc2lem  32921  dfmgc2  32922  pwrssmgc  32926  mgcf1o  32929  chnso  32940  mndlrinvb  32966  mndlactf1  32967  mndractf1  32969  gsummpt2co  32988  gsumwrd2dccatlem  33006  tocyccntz  33101  cycpmconjs  33113  conjga  33127  urpropd  33183  elrgspnlem2  33194  elrgspnlem4  33196  elrgspnsubrunlem2  33199  elrgspnsubrun  33200  erler  33216  rlocaddval  33219  rlocmulval  33220  rlocf1  33224  domnprodn0  33226  rrgsubm  33234  subrdom  33235  isdrng4  33245  suborng  33293  eqgvscpbl  33321  dvdsruasso  33356  nsgmgclem  33382  nsgmgc  33383  nsgqusf1olem2  33385  nsgqusf1olem3  33386  lmhmqusker  33388  intlidl  33391  rhmquskerlem  33396  elrspunidl  33399  elrspunsn  33400  idlinsubrg  33402  rhmimaidl  33403  drngidl  33404  prmidl2  33412  idlmulssprm  33413  isprmidlc  33418  rhmpreimaprmidl  33422  qsidomlem1  33423  qsidomlem2  33424  ssdifidllem  33427  ssdifidlprm  33429  mxidlprm  33441  mxidlirredi  33442  ssmxidllem  33444  opprlidlabs  33456  qsdrngi  33466  rsprprmprmidl  33493  rsprprmprmidlb  33494  rprmirred  33502  rprmirredb  33503  rprmdvdsprod  33505  1arithidom  33508  1arithufdlem3  33517  1arithufdlem4  33518  r1plmhm  33575  r1pquslmic  33576  ply1degltdimlem  33618  ply1degltdim  33619  lindsun  33621  lbsdiflsp0  33622  fedgmullem1  33625  fedgmul  33627  lactlmhm  33630  assalactf1o  33631  extdg1id  33661  fldextrspunlsplem  33668  fldextrspunlsp  33669  minplyirred  33701  algextdeglem8  33714  constrextdg2lem  33738  constrextdg2  33739  constrfiss  33741  constrsdrg  33765  cos9thpiminplylem2  33773  zart0  33869  pstmxmet  33887  ordtconnlem1  33914  esumiun  34084  dya2iocnei  34273  omssubadd  34291  actfunsnf1o  34595  fsum2dsub  34598  reprsuc  34606  reprinfz1  34613  reprpmtf1o  34617  breprexplema  34621  circlemeth  34631  hgt750lemb  34647  cusgr3cyclex  35123  resconn  35233  pibt2  37405  uncf  37593  unccur  37597  fin2so  37601  matunitlindflem1  37610  poimirlem6  37620  poimirlem7  37621  poimirlem25  37639  poimirlem28  37642  poimirlem31  37645  poimirlem32  37646  broucube  37648  ismblfin  37655  mbfposadd  37661  itg2gt0cn  37669  ftc1anclem7  37693  ftc1anc  37695  cover2  37709  indexa  37727  filbcmb  37734  seqpo  37741  incsequz  37742  isbnd2  37777  ghomco  37885  unichnidl  38025  isfldidl  38062  dihvalc  41227  dihvalb  41231  uzindd  41965  aks4d1p8  42075  evlselv  42575  fsuppind  42578  radcnvrat  44303  rexabslelem  45414  rexlimddv2  45821  dvnprodlem2  45945  etransclem46  46278  isgrtri  47942  grlimgrtri  47995  lubeldm2  48944  glbeldm2  48945  thincciso2  49444  aacllem  49790