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  3151  rspc4v  3611  f1elima  7241  fnfvof  7673  frxp3  8133  oecl  8504  oaass  8528  oen0  8553  oeworde  8560  omabs  8618  oiiniseg  9493  cardinfima  10057  fpwwe2lem11  10601  ltmul12a  12045  eluzp1m1  12826  lbzbi  12902  qreccl  12935  xrlttr  13107  elfzodifsumelfzo  13699  quoremnn0  13825  incexc2  15811  mertens  15859  ndvdsadd  16387  nn0seqcvgd  16547  isprm3  16660  isprm7  16685  pcval  16822  prdsval  17425  evlfcl  18190  ghmqusnsg  19221  ghmquskerlem3  19225  frgpup1  19712  frgpup3lem  19714  ghmcmn  19768  gsumval3  19844  gsumzoppg  19881  ablfaclem2  20025  gsumdixp  20235  rhmpreimaidl  21194  rhmqusnsg  21202  frlmgsum  21688  psrass1lem  21848  psrass1  21880  psdmul  22060  evls1maplmhm  22271  m2cpminvid2  22649  pmatcollpw2lem  22671  chcoeffeqlem  22779  neissex  23021  neiptopnei  23026  dissnlocfin  23423  tx1stc  23544  kqreglem1  23635  xpstopnlem1  23703  alexsublem  23938  metuel2  24460  icoopnst  24843  iocopnst  24844  volcn  25514  mbflimsup  25574  mbflim  25576  itg1addlem4  25607  itg1addlem5  25608  itg1climres  25622  limcflf  25789  dvcobr  25856  dvcobrOLD  25857  dvcnvlem  25887  dvfsumge  25935  mdegmullem  25990  plyeq0lem  26122  plypf1  26124  mtestbdd  26321  mbfulm  26322  fsumdvdscom  27102  muinv  27110  logfaclbnd  27140  logexprlim  27143  dchrinv  27179  lgsval3  27233  2sqmo  27355  rpvmasum2  27430  dchrisum0lem1  27434  dchrisum0  27438  selberg  27466  selberg3lem1  27475  selberg34r  27489  pntsval2  27494  nosupbnd1lem5  27631  noinfbnd1lem5  27646  nocvxminlem  27696  oldbday  27819  peano5uzs  28299  iscgrglt  28448  ercgrg  28451  legso  28533  oppperpex  28687  hpgerlem  28699  trgcopyeu  28740  dfcgra2  28764  inaghl  28779  colinearalg  28844  axeuclid  28897  axcontlem2  28899  axcontlem7  28904  wlkiswwlksupgr2  29814  grpoidinvlem4  30443  ipblnfi  30791  shmodsi  31325  eighmorth  31900  kbass5  32056  kbass6  32057  dmdmd  32236  atom1d  32289  mdsymlem2  32340  mdsymlem3  32341  mdsymlem4  32342  mdsymlem5  32343  fmptco1f1o  32564  2ndresdju  32580  fnpreimac  32602  fsumiunle  32761  s3f1  32875  swrdf1  32885  dfmgc2lem  32928  dfmgc2  32929  pwrssmgc  32933  mgcf1o  32936  chnso  32947  mndlrinvb  32973  mndlactf1  32974  mndractf1  32976  gsummpt2co  32995  gsumwrd2dccatlem  33013  tocyccntz  33108  cycpmconjs  33120  conjga  33134  urpropd  33190  elrgspnlem2  33201  elrgspnlem4  33203  elrgspnsubrunlem2  33206  elrgspnsubrun  33207  erler  33223  rlocaddval  33226  rlocmulval  33227  rlocf1  33231  domnprodn0  33233  rrgsubm  33241  subrdom  33242  isdrng4  33252  suborng  33300  eqgvscpbl  33328  dvdsruasso  33363  nsgmgclem  33389  nsgmgc  33390  nsgqusf1olem2  33392  nsgqusf1olem3  33393  lmhmqusker  33395  intlidl  33398  rhmquskerlem  33403  elrspunidl  33406  elrspunsn  33407  idlinsubrg  33409  rhmimaidl  33410  drngidl  33411  prmidl2  33419  idlmulssprm  33420  isprmidlc  33425  rhmpreimaprmidl  33429  qsidomlem1  33430  qsidomlem2  33431  ssdifidllem  33434  ssdifidlprm  33436  mxidlprm  33448  mxidlirredi  33449  ssmxidllem  33451  opprlidlabs  33463  qsdrngi  33473  rsprprmprmidl  33500  rsprprmprmidlb  33501  rprmirred  33509  rprmirredb  33510  rprmdvdsprod  33512  1arithidom  33515  1arithufdlem3  33524  1arithufdlem4  33525  r1plmhm  33582  r1pquslmic  33583  ply1degltdimlem  33625  ply1degltdim  33626  lindsun  33628  lbsdiflsp0  33629  fedgmullem1  33632  fedgmul  33634  lactlmhm  33637  assalactf1o  33638  extdg1id  33668  fldextrspunlsplem  33675  fldextrspunlsp  33676  minplyirred  33708  algextdeglem8  33721  constrextdg2lem  33745  constrextdg2  33746  constrfiss  33748  constrsdrg  33772  cos9thpiminplylem2  33780  zart0  33876  pstmxmet  33894  ordtconnlem1  33921  esumiun  34091  dya2iocnei  34280  omssubadd  34298  actfunsnf1o  34602  fsum2dsub  34605  reprsuc  34613  reprinfz1  34620  reprpmtf1o  34624  breprexplema  34628  circlemeth  34638  hgt750lemb  34654  cusgr3cyclex  35130  resconn  35240  pibt2  37412  uncf  37600  unccur  37604  fin2so  37608  matunitlindflem1  37617  poimirlem6  37627  poimirlem7  37628  poimirlem25  37646  poimirlem28  37649  poimirlem31  37652  poimirlem32  37653  broucube  37655  ismblfin  37662  mbfposadd  37668  itg2gt0cn  37676  ftc1anclem7  37700  ftc1anc  37702  cover2  37716  indexa  37734  filbcmb  37741  seqpo  37748  incsequz  37749  isbnd2  37784  ghomco  37892  unichnidl  38032  isfldidl  38069  dihvalc  41234  dihvalb  41238  uzindd  41972  aks4d1p8  42082  evlselv  42582  fsuppind  42585  radcnvrat  44310  rexabslelem  45421  rexlimddv2  45828  dvnprodlem2  45952  etransclem46  46285  isgrtri  47946  grlimgrtri  47999  lubeldm2  48948  glbeldm2  48949  thincciso2  49448  aacllem  49794