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  3153  rspc4v  3596  f1elima  7209  fnfvof  7639  frxp3  8093  oecl  8464  oaass  8488  oen0  8514  oeworde  8521  omabs  8579  oiiniseg  9438  cardinfima  10007  fpwwe2lem11  10552  ltmul12a  11997  eluzp1m1  12777  lbzbi  12849  qreccl  12882  xrlttr  13054  elfzodifsumelfzo  13647  quoremnn0  13776  incexc2  15761  mertens  15809  ndvdsadd  16337  nn0seqcvgd  16497  isprm3  16610  isprm7  16635  pcval  16772  prdsval  17375  evlfcl  18145  chnso  18547  ghmqusnsg  19211  ghmquskerlem3  19215  frgpup1  19704  frgpup3lem  19706  ghmcmn  19760  gsumval3  19836  gsumzoppg  19873  ablfaclem2  20017  gsumdixp  20254  suborng  20809  rhmpreimaidl  21232  rhmqusnsg  21240  frlmgsum  21727  psrass1lem  21888  psrass1  21919  psdmul  22109  evls1maplmhm  22321  m2cpminvid2  22699  pmatcollpw2lem  22721  chcoeffeqlem  22829  neissex  23071  neiptopnei  23076  dissnlocfin  23473  tx1stc  23594  kqreglem1  23685  xpstopnlem1  23753  alexsublem  23988  metuel2  24509  icoopnst  24892  iocopnst  24893  volcn  25563  mbflimsup  25623  mbflim  25625  itg1addlem4  25656  itg1addlem5  25657  itg1climres  25671  limcflf  25838  dvcobr  25905  dvcobrOLD  25906  dvcnvlem  25936  dvfsumge  25984  mdegmullem  26039  plyeq0lem  26171  plypf1  26173  mtestbdd  26370  mbfulm  26371  fsumdvdscom  27151  muinv  27159  logfaclbnd  27189  logexprlim  27192  dchrinv  27228  lgsval3  27282  2sqmo  27404  rpvmasum2  27479  dchrisum0lem1  27483  dchrisum0  27487  selberg  27515  selberg3lem1  27524  selberg34r  27538  pntsval2  27543  nosupbnd1lem5  27680  noinfbnd1lem5  27695  nocvxminlem  27750  oldbday  27897  peano5uzs  28400  iscgrglt  28586  ercgrg  28589  legso  28671  oppperpex  28825  hpgerlem  28837  trgcopyeu  28878  dfcgra2  28902  inaghl  28917  colinearalg  28983  axeuclid  29036  axcontlem2  29038  axcontlem7  29043  wlkiswwlksupgr2  29950  grpoidinvlem4  30582  ipblnfi  30930  shmodsi  31464  eighmorth  32039  kbass5  32195  kbass6  32196  dmdmd  32375  atom1d  32428  mdsymlem2  32479  mdsymlem3  32480  mdsymlem4  32481  mdsymlem5  32482  fmptco1f1o  32711  2ndresdju  32727  fnpreimac  32749  fsumiunle  32910  s3f1  33029  swrdf1  33038  dfmgc2lem  33077  dfmgc2  33078  pwrssmgc  33082  mgcf1o  33085  mndlrinvb  33107  mndlactf1  33108  mndractf1  33110  gsummpt2co  33131  gsumwrd2dccatlem  33159  tocyccntz  33226  cycpmconjs  33238  conjga  33252  fxpsubrg  33256  urpropd  33313  elrgspnlem2  33325  elrgspnlem4  33327  elrgspnsubrunlem2  33330  elrgspnsubrun  33331  erler  33347  rlocaddval  33350  rlocmulval  33351  rlocf1  33355  domnprodn0  33357  domnprodeq0  33358  rrgsubm  33366  subrdom  33367  isdrng4  33377  eqgvscpbl  33431  dvdsruasso  33466  nsgmgclem  33492  nsgmgc  33493  nsgqusf1olem2  33495  nsgqusf1olem3  33496  lmhmqusker  33498  intlidl  33501  rhmquskerlem  33506  elrspunidl  33509  elrspunsn  33510  idlinsubrg  33512  rhmimaidl  33513  drngidl  33514  prmidl2  33522  idlmulssprm  33523  isprmidlc  33528  rhmpreimaprmidl  33532  qsidomlem1  33533  qsidomlem2  33534  ssdifidllem  33537  ssdifidlprm  33539  mxidlprm  33551  mxidlirredi  33552  ssmxidllem  33554  opprlidlabs  33566  qsdrngi  33576  rsprprmprmidl  33603  rsprprmprmidlb  33604  rprmirred  33612  rprmirredb  33613  rprmdvdsprod  33615  1arithidom  33618  1arithufdlem3  33627  1arithufdlem4  33628  deg1prod  33664  r1plmhm  33691  r1pquslmic  33692  extvfvcl  33701  mplvrpmga  33710  mplvrpmmhm  33711  mplvrpmrhm  33712  vieta  33736  ply1degltdimlem  33779  ply1degltdim  33780  lindsun  33782  lbsdiflsp0  33783  fedgmullem1  33786  fedgmul  33788  lactlmhm  33791  assalactf1o  33792  extdg1id  33823  fldextrspunlsplem  33830  fldextrspunlsp  33831  extdgfialglem2  33850  extdgfialg  33851  minplyirred  33868  algextdeglem8  33881  constrextdg2lem  33905  constrextdg2  33906  constrfiss  33908  constrsdrg  33932  cos9thpiminplylem2  33940  zart0  34036  pstmxmet  34054  ordtconnlem1  34081  esumiun  34251  dya2iocnei  34439  omssubadd  34457  actfunsnf1o  34761  fsum2dsub  34764  reprsuc  34772  reprinfz1  34779  reprpmtf1o  34783  breprexplema  34787  circlemeth  34797  hgt750lemb  34813  cusgr3cyclex  35330  resconn  35440  pibt2  37622  uncf  37800  unccur  37804  fin2so  37808  matunitlindflem1  37817  poimirlem6  37827  poimirlem7  37828  poimirlem25  37846  poimirlem28  37849  poimirlem31  37852  poimirlem32  37853  broucube  37855  ismblfin  37862  mbfposadd  37868  itg2gt0cn  37876  ftc1anclem7  37900  ftc1anc  37902  cover2  37916  indexa  37934  filbcmb  37941  seqpo  37948  incsequz  37949  isbnd2  37984  ghomco  38092  unichnidl  38232  isfldidl  38269  dihvalc  41493  dihvalb  41497  uzindd  42231  aks4d1p8  42341  evlselv  42830  fsuppind  42833  radcnvrat  44555  rexabslelem  45662  rexlimddv2  46067  dvnprodlem2  46191  etransclem46  46524  isgrtri  48189  grlimgrtri  48249  lubeldm2  49201  glbeldm2  49202  thincciso2  49700  aacllem  50046