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 206  df-an 396

This theorem is referenced by:  anass  468  anabss3  671  biadanid  819  f1elima  7130  fnfvof  7541  oecl  8343  oaass  8368  oen0  8393  oeworde  8400  omabs  8455  oiiniseg  9253  cardinfima  9837  fpwwe2lem11  10381  ltmul12a  11814  eluzp1m1  12590  lbzbi  12658  qreccl  12691  xrlttr  12856  elfzodifsumelfzo  13434  quoremnn0  13557  incexc2  15531  mertens  15579  ndvdsadd  16100  nn0seqcvgd  16256  isprm3  16369  isprm7  16394  pcval  16526  prdsval  17147  evlfcl  17921  frgpup1  19362  frgpup3lem  19364  ghmcmn  19414  gsumval3  19489  gsumzoppg  19526  ablfaclem2  19670  gsumdixp  19829  frlmgsum  20960  psrass1lemOLD  21124  psrass1lem  21127  psrass1  21155  m2cpminvid2  21885  pmatcollpw2lem  21907  chcoeffeqlem  22015  neissex  22259  neiptopnei  22264  dissnlocfin  22661  tx1stc  22782  kqreglem1  22873  xpstopnlem1  22941  alexsublem  23176  metuel2  23702  icoopnst  24083  iocopnst  24084  volcn  24751  mbflimsup  24811  mbflim  24813  itg1addlem4  24844  itg1addlem4OLD  24845  itg1addlem5  24846  itg1climres  24860  limcflf  25026  dvcobr  25091  dvcnvlem  25121  dvfsumge  25167  mdegmullem  25224  plyeq0lem  25352  plypf1  25354  mtestbdd  25545  mbfulm  25546  fsumdvdscom  26315  muinv  26323  logfaclbnd  26351  logexprlim  26354  dchrinv  26390  lgsval3  26444  2sqmo  26566  rpvmasum2  26641  dchrisum0lem1  26645  dchrisum0  26649  selberg  26677  selberg3lem1  26686  selberg34r  26700  pntsval2  26705  iscgrglt  26856  ercgrg  26859  legso  26941  oppperpex  27095  hpgerlem  27107  trgcopyeu  27148  dfcgra2  27172  inaghl  27187  colinearalg  27259  axeuclid  27312  axcontlem2  27314  axcontlem7  27319  wlkiswwlksupgr2  28221  grpoidinvlem4  28848  ipblnfi  29196  shmodsi  29730  eighmorth  30305  kbass5  30461  kbass6  30462  dmdmd  30641  atom1d  30694  mdsymlem2  30745  mdsymlem3  30746  mdsymlem4  30747  mdsymlem5  30748  fmptco1f1o  30947  2ndresdju  30965  fnpreimac  30987  fsumiunle  31122  s3f1  31200  swrdf1  31207  dfmgc2lem  31252  dfmgc2  31253  pwrssmgc  31257  mgcf1o  31260  gsummpt2co  31287  tocyccntz  31390  cycpmconjs  31402  suborng  31493  eqgvscpbl  31529  nsgmgclem  31575  nsgmgc  31576  nsgqusf1olem2  31578  nsgqusf1olem3  31579  intlidl  31581  rhmpreimaidl  31582  elrspunidl  31585  idlinsubrg  31587  rhmimaidl  31588  prmidl2  31595  idlmulssprm  31596  isprmidlc  31602  rhmpreimaprmidl  31606  qsidomlem1  31607  qsidomlem2  31608  mxidlprm  31619  ssmxidllem  31620  lindsun  31685  lbsdiflsp0  31686  fedgmullem1  31689  fedgmul  31691  extdg1id  31717  zart0  31808  pstmxmet  31826  ordtconnlem1  31853  esumiun  32041  dya2iocnei  32228  omssubadd  32246  actfunsnf1o  32563  fsum2dsub  32566  reprsuc  32574  reprinfz1  32581  reprpmtf1o  32585  breprexplema  32589  circlemeth  32599  hgt750lemb  32615  cusgr3cyclex  33077  resconn  33187  nosupbnd1lem5  33894  noinfbnd1lem5  33909  nocvxminlem  33951  oldbday  34060  pibt2  35567  uncf  35735  unccur  35739  fin2so  35743  matunitlindflem1  35752  poimirlem6  35762  poimirlem7  35763  poimirlem25  35781  poimirlem28  35784  poimirlem31  35787  poimirlem32  35788  broucube  35790  ismblfin  35797  mbfposadd  35803  itg2gt0cn  35811  ftc1anclem7  35835  ftc1anc  35837  cover2  35851  indexa  35870  filbcmb  35877  seqpo  35884  incsequz  35885  isbnd2  35920  ghomco  36028  unichnidl  36168  isfldidl  36205  dihvalc  39226  dihvalb  39230  uzindd  39965  aks4d1p8  40075  fsuppind  40259  radcnvrat  41885  reximddv3  42653  rexabslelem  42912  rexlimddv2  43318  dvnprodlem2  43442  etransclem46  43775  lubeldm2  46202  glbeldm2  46203  aacllem  46457