Theorem anasss 470

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 423	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp32 422	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  anass  472  anabss3  675  f1elima  7044  fnfvof  7453  oecl  8205  oaass  8230  oen0  8255  oeworde  8262  omabs  8317  oiiniseg  9082  cardinfima  9609  fpwwe2lem11  10153  ltmul12a  11586  eluzp1m1  12362  lbzbi  12430  qreccl  12463  xrlttr  12628  elfzodifsumelfzo  13206  quoremnn0  13327  incexc2  15298  mertens  15346  ndvdsadd  15867  nn0seqcvgd  16023  isprm3  16136  isprm7  16161  pcval  16293  prdsval  16843  evlfcl  17600  frgpup1  19031  frgpup3lem  19033  ghmcmn  19083  gsumval3  19158  gsumzoppg  19195  ablfaclem2  19339  gsumdixp  19493  frlmgsum  20600  psrass1lemOLD  20765  psrass1lem  20768  psrass1  20796  m2cpminvid2  21518  pmatcollpw2lem  21540  chcoeffeqlem  21648  neissex  21890  neiptopnei  21895  dissnlocfin  22292  tx1stc  22413  kqreglem1  22504  xpstopnlem1  22572  alexsublem  22807  metuel2  23330  icoopnst  23703  iocopnst  23704  volcn  24370  mbflimsup  24430  mbflim  24432  itg1addlem4  24463  itg1addlem4OLD  24464  itg1addlem5  24465  itg1climres  24479  limcflf  24645  dvcobr  24710  dvcnvlem  24740  dvfsumge  24786  mdegmullem  24843  plyeq0lem  24971  plypf1  24973  mtestbdd  25164  mbfulm  25165  fsumdvdscom  25934  muinv  25942  logfaclbnd  25970  logexprlim  25973  dchrinv  26009  lgsval3  26063  2sqmo  26185  rpvmasum2  26260  dchrisum0lem1  26264  dchrisum0  26268  selberg  26296  selberg3lem1  26305  selberg34r  26319  pntsval2  26324  iscgrglt  26472  ercgrg  26475  legso  26557  oppperpex  26711  hpgerlem  26723  trgcopyeu  26764  dfcgra2  26788  inaghl  26803  colinearalg  26868  axeuclid  26921  axcontlem2  26923  axcontlem7  26928  wlkiswwlksupgr2  27827  grpoidinvlem4  28454  ipblnfi  28802  shmodsi  29336  eighmorth  29911  kbass5  30067  kbass6  30068  dmdmd  30247  atom1d  30300  mdsymlem2  30351  mdsymlem3  30352  mdsymlem4  30353  mdsymlem5  30354  biadanid  30400  fmptco1f1o  30554  2ndresdju  30572  fnpreimac  30595  fsumiunle  30730  s3f1  30808  swrdf1  30815  dfmgc2lem  30862  dfmgc2  30863  pwrssmgc  30867  mgcf1o  30870  gsummpt2co  30897  tocyccntz  31000  cycpmconjs  31012  suborng  31103  eqgvscpbl  31134  nsgmgclem  31180  nsgmgc  31181  nsgqusf1olem2  31183  nsgqusf1olem3  31184  intlidl  31186  rhmpreimaidl  31187  elrspunidl  31190  idlinsubrg  31192  rhmimaidl  31193  prmidl2  31200  idlmulssprm  31201  isprmidlc  31207  rhmpreimaprmidl  31211  qsidomlem1  31212  qsidomlem2  31213  mxidlprm  31224  ssmxidllem  31225  lindsun  31290  lbsdiflsp0  31291  fedgmullem1  31294  fedgmul  31296  extdg1id  31322  zart0  31413  pstmxmet  31431  ordtconnlem1  31458  esumiun  31644  dya2iocnei  31831  omssubadd  31849  actfunsnf1o  32166  fsum2dsub  32169  reprsuc  32177  reprinfz1  32184  reprpmtf1o  32188  breprexplema  32192  circlemeth  32202  hgt750lemb  32218  cusgr3cyclex  32681  resconn  32791  nosupbnd1lem5  33570  noinfbnd1lem5  33585  nocvxminlem  33627  oldbday  33736  pibt2  35243  uncf  35411  unccur  35415  fin2so  35419  matunitlindflem1  35428  poimirlem6  35438  poimirlem7  35439  poimirlem25  35457  poimirlem28  35460  poimirlem31  35463  poimirlem32  35464  broucube  35466  ismblfin  35473  mbfposadd  35479  itg2gt0cn  35487  ftc1anclem7  35511  ftc1anc  35513  cover2  35527  indexa  35546  filbcmb  35553  seqpo  35560  incsequz  35561  isbnd2  35596  ghomco  35704  unichnidl  35844  isfldidl  35881  dihvalc  38902  dihvalb  38906  uzindd  39637  fsuppind  39898  radcnvrat  41510  reximddv3  42278  rexabslelem  42536  rexlimddv2  42946  dvnprodlem2  43070  etransclem46  43403  aacllem  46005