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  3157  rspc4v  3621  f1elima  7255  fnfvof  7686  frxp3  8148  oecl  8547  oaass  8571  oen0  8596  oeworde  8603  omabs  8661  oiiniseg  9545  cardinfima  10109  fpwwe2lem11  10653  ltmul12a  12095  eluzp1m1  12876  lbzbi  12950  qreccl  12983  xrlttr  13154  elfzodifsumelfzo  13745  quoremnn0  13871  incexc2  15852  mertens  15900  ndvdsadd  16427  nn0seqcvgd  16587  isprm3  16700  isprm7  16725  pcval  16862  prdsval  17467  evlfcl  18232  ghmqusnsg  19263  ghmquskerlem3  19267  frgpup1  19754  frgpup3lem  19756  ghmcmn  19810  gsumval3  19886  gsumzoppg  19923  ablfaclem2  20067  gsumdixp  20277  rhmpreimaidl  21236  rhmqusnsg  21244  frlmgsum  21730  psrass1lem  21890  psrass1  21922  psdmul  22102  evls1maplmhm  22313  m2cpminvid2  22691  pmatcollpw2lem  22713  chcoeffeqlem  22821  neissex  23063  neiptopnei  23068  dissnlocfin  23465  tx1stc  23586  kqreglem1  23677  xpstopnlem1  23745  alexsublem  23980  metuel2  24502  icoopnst  24885  iocopnst  24886  volcn  25557  mbflimsup  25617  mbflim  25619  itg1addlem4  25650  itg1addlem5  25651  itg1climres  25665  limcflf  25832  dvcobr  25899  dvcobrOLD  25900  dvcnvlem  25930  dvfsumge  25978  mdegmullem  26033  plyeq0lem  26165  plypf1  26167  mtestbdd  26364  mbfulm  26365  fsumdvdscom  27145  muinv  27153  logfaclbnd  27183  logexprlim  27186  dchrinv  27222  lgsval3  27276  2sqmo  27398  rpvmasum2  27473  dchrisum0lem1  27477  dchrisum0  27481  selberg  27509  selberg3lem1  27518  selberg34r  27532  pntsval2  27537  nosupbnd1lem5  27674  noinfbnd1lem5  27689  nocvxminlem  27739  oldbday  27856  peano5uzs  28307  iscgrglt  28439  ercgrg  28442  legso  28524  oppperpex  28678  hpgerlem  28690  trgcopyeu  28731  dfcgra2  28755  inaghl  28770  colinearalg  28835  axeuclid  28888  axcontlem2  28890  axcontlem7  28895  wlkiswwlksupgr2  29805  grpoidinvlem4  30434  ipblnfi  30782  shmodsi  31316  eighmorth  31891  kbass5  32047  kbass6  32048  dmdmd  32227  atom1d  32280  mdsymlem2  32331  mdsymlem3  32332  mdsymlem4  32333  mdsymlem5  32334  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  urpropd  33173  elrgspnlem2  33184  elrgspnlem4  33186  elrgspnsubrunlem2  33189  elrgspnsubrun  33190  erler  33206  rlocaddval  33209  rlocmulval  33210  rlocf1  33214  domnprodn0  33216  rrgsubm  33224  subrdom  33225  isdrng4  33235  suborng  33283  eqgvscpbl  33311  dvdsruasso  33346  nsgmgclem  33372  nsgmgc  33373  nsgqusf1olem2  33375  nsgqusf1olem3  33376  lmhmqusker  33378  intlidl  33381  rhmquskerlem  33386  elrspunidl  33389  elrspunsn  33390  idlinsubrg  33392  rhmimaidl  33393  drngidl  33394  prmidl2  33402  idlmulssprm  33403  isprmidlc  33408  rhmpreimaprmidl  33412  qsidomlem1  33413  qsidomlem2  33414  ssdifidllem  33417  ssdifidlprm  33419  mxidlprm  33431  mxidlirredi  33432  ssmxidllem  33434  opprlidlabs  33446  qsdrngi  33456  rsprprmprmidl  33483  rsprprmprmidlb  33484  rprmirred  33492  rprmirredb  33493  rprmdvdsprod  33495  1arithidom  33498  1arithufdlem3  33507  1arithufdlem4  33508  r1plmhm  33565  r1pquslmic  33566  ply1degltdimlem  33608  ply1degltdim  33609  lindsun  33611  lbsdiflsp0  33612  fedgmullem1  33615  fedgmul  33617  lactlmhm  33620  assalactf1o  33621  extdg1id  33653  fldextrspunlsplem  33660  fldextrspunlsp  33661  minplyirred  33691  algextdeglem8  33704  constrextdg2lem  33728  constrextdg2  33729  constrfiss  33731  constrsdrg  33755  cos9thpiminplylem2  33763  zart0  33856  pstmxmet  33874  ordtconnlem1  33901  esumiun  34071  dya2iocnei  34260  omssubadd  34278  actfunsnf1o  34582  fsum2dsub  34585  reprsuc  34593  reprinfz1  34600  reprpmtf1o  34604  breprexplema  34608  circlemeth  34618  hgt750lemb  34634  cusgr3cyclex  35104  resconn  35214  pibt2  37381  uncf  37569  unccur  37573  fin2so  37577  matunitlindflem1  37586  poimirlem6  37596  poimirlem7  37597  poimirlem25  37615  poimirlem28  37618  poimirlem31  37621  poimirlem32  37622  broucube  37624  ismblfin  37631  mbfposadd  37637  itg2gt0cn  37645  ftc1anclem7  37669  ftc1anc  37671  cover2  37685  indexa  37703  filbcmb  37710  seqpo  37717  incsequz  37718  isbnd2  37753  ghomco  37861  unichnidl  38001  isfldidl  38038  dihvalc  41198  dihvalb  41202  uzindd  41936  aks4d1p8  42046  evlselv  42557  fsuppind  42560  radcnvrat  44286  rexabslelem  45393  rexlimddv2  45800  dvnprodlem2  45924  etransclem46  46257  isgrtri  47903  grlimgrtri  47956  lubeldm2  48878  glbeldm2  48879  thincciso2  49289  aacllem  49613