Theorem 3anass 1111

Description: Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.)

Assertion

Ref	Expression
3anass	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

Proof of Theorem 3anass

Step	Hyp	Ref	Expression
1		df-3an 1105	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		anass 474	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3	1, 2	bitri 278	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anan12  1112  3ancoma  1115  anandi3  1119  4anpull2OLD  1383  3biant1d  1509  an33rean  1514  cad1  1650  3exdistr  1993  ceqsex2  3500  ceqsex2v  3501  ceqsex3v  3502  ceqsex4v  3503  ceqsex6v  3504  ceqsex8v  3505  2reu5lem1  3713  2reu5lem2  3714  2reu5lem3  3715  eldifpr  4619  rexdifpr  4620  trel3  5221  2rbropap  5536  ordelord  6374  dflim2  6411  dff1o4  6822  foco2  7098  brfvopab  7466  eloprabga  7518  ndmovass  7598  ndmovdistr  7599  dflim3  7842  dflim4  7843  frxp2  8140  mpoxopovel  8216  dfsmo2  8334  dfrecs3  8359  oeeui  8590  naddasslem2  8684  ecopovtrn  8820  elixp2  8908  elixp  8911  mptelixpg  8942  dif1en  9156  ssfi  9167  sbthfilem  9192  eqinf  9455  zorn2lem7  10537  grothprim  10876  grothtsk  10877  divmulasscom  11953  muldivdir  11964  divmuldiv  11972  sup3  12229  dfnn3  12304  prime  12735  eluz2  12926  raluz2  12979  elixx1  13440  elixx3g  13444  elioo2  13472  elioo5  13489  elicc4  13499  iccneg  13558  icoshft  13559  difreicc  13570  elfz1  13599  elfz  13600  elfz2  13601  elfzm11  13683  elfz2nn0  13706  elfzo2  13750  elfzo3  13765  lbfzo0  13788  fzo1lb  13802  1elfzo1  13803  fzind2  13877  zmodid2  13993  hashgt23el  14522  swrdnd2  14758  swrdnd0  14760  swrdccatin1  14827  swrdccat  14837  repswswrd  14888  swrdco  14941  2swrd2eqwrdeq  15059  rediv  15251  imdiv  15258  cosmul  16294  bitsval  16547  bitsmod  16559  bitscmp  16561  smueqlem  16613  dfgcd2  16669  lcmneg  16726  lcmftp  16759  coprmgcdb  16772  divgcdcoprmex  16789  cncongr1  16790  cncongr2  16791  difsqpwdvds  17012  oddprmdvds  17028  elgz  17056  xpsfrnel  17681  xpsfrnel2  17683  ismre  17707  mreexexlem4d  17768  iscatd2  17802  isssc  17942  eldmcoa  18187  isdrs  18422  isipodrs  18658  mgmsscl  18768  ismhm  18927  mhmpropd  18934  issubm  18945  issubmndb  18947  submacs  18970  issubg  19283  eqglact  19338  eqgid  19339  ecqusaddd  19354  ecqusaddcl  19355  pgrpsubgsymgbi  19569  isslw  19769  efgsdm  19891  mulgmhm  19988  mulgghm  19989  dmdprd  20161  dprdw  20173  subgdmdprd  20197  dmdprdpr  20212  isomnd  20284  isrng  20323  issrg  20361  srglmhm  20394  srgrmhm  20395  isring  20410  dfring3  20465  ringlghm  20490  dfrhm2  20651  isrhm0  20653  crngrhmfo  20673  issubrng  20746  issubrg3  20799  isdomn3  20913  isdrng3  20954  issdrg  20992  sdrgacs  21005  islmod  21086  lsspropd  21239  islmhm  21249  islbs  21298  lbspropd  21321  isfieldidl  21487  isfieldidl2  21488  qusmulrng  21525  rngqiprngghmlem3  21532  rngqiprnglinlem3  21536  rngqiprnglin  21545  isprmidl  21566  isprmidlc  21575  cnfldfunALT  21640  isphl  21881  elocv  21921  isobs  21973  mat1dimscm  22737  scmatghm  22795  scmatmhm  22796  ma1repvcl  22832  smadiadetr  22937  mat2pmatghm  22995  mat2pmatmul  22996  decpmatmulsumfsupp  23038  pm2mpghm  23081  pm2mpmhmlem1  23083  neindisj  23382  lmbrf  23525  hauscmplem  23671  llyi  23740  subislly  23747  islocfin  23783  uptx  23891  txcn  23892  qtopeu  23982  elmptrab  24093  isfbas  24095  trfil2  24153  flimcls  24251  cnextcn  24333  xmetec  24700  ngppropd  24903  ngpocelbl  24970  bl2ioo  25058  xrtgioo  25073  om1elbas  25300  elpi1  25313  isclm  25332  isclmp  25365  isncvsngp  25417  iscph  25438  tcphcph  25505  lmmbr2  25527  lmmbrf  25530  iscau2  25545  caussi  25565  lmclim  25571  bcthlem1  25592  srabn  25628  ishl2  25638  evthicc2  25728  ovolfioo  25735  ovolficc  25736  iblcnlem1  26055  iblrelem  26058  iblre  26061  iblcn  26066  isuc1p  26406  ismon1p  26408  ellogrn  26836  logreclem  27039  atandm  27153  atandm2  27154  atandm3  27155  atans2  27208  dmarea  27234  dchrelbas4  27519  lgsmodeq  27618  lgsmulsqcoprm  27619  nocvxminlem  28059  cutcuts  28086  cutbday  28089  addcuts2  28284  mulcut2  28438  ax5seg  29435  eengtrkg  29483  uspgredg2v  29724  nb3grpr2  29883  isrusgr0  30066  rusgrprop0  30067  ewlkprop  30103  wksfval  30109  wlkeq  30133  wlkson  30154  wlkonprop  30156  upgr2wlk  30166  upgrtrls  30203  upgristrl  30204  wksonproplem  30206  pthsfval  30223  ispth  30225  dfpth2  30233  isspthonpth  30254  uhgrwkspth  30260  usgr2wlkspth  30264  crctcshwlkn0lem4  30321  wspthnp  30358  wwlknon  30365  wwlksnextwrd  30405  wwlksnextinj  30407  wspthsnwspthsnon  30424  umgr2adedgwlk  30453  umgr2adedgwlkon  30454  umgr2adedgwlkonALT  30455  umgr2adedgspth  30456  s3wwlks2on  30464  sps3wwlks2on  30465  wpthswwlks2on  30472  usgr2wspthons3  30475  usgr2wspthon  30476  elwwlks2  30477  elwspths2spth  30478  rusgrnumwwlkl1  30479  rusgrnumwwlkslem  30480  isclwwlk  30494  clwwlkbp  30495  clwlkclwwlklem3  30511  isclwwlknx  30546  clwwlknp  30547  clwwlkn1  30551  clwwlkn2  30554  clwwlkwwlksb  30564  clwwlknonel  30605  0pth  30635  frcond4  30790  1to3vfriswmgr  30800  3cyclfrgr  30808  frgrwopreglem5  30841  2clwwlk2clwwlk  30870  numclwlk1lem1  30889  numclwwlk6  30910  ajval  31382  issh  31729  dmadjss  32408  adjeu  32410  adjval  32411  isst  32734  ishst  32735  xrdifh  33291  nndiffz1  33297  xdivpnfrp  33418  isslmd  33682  ismxidl  33906  ressply1mon1p  34019  isrrext  34551  ismntop  34577  isros  34720  issros  34727  issibf  34885  eulerpartleme  34915  eulerpartlemt0  34921  probun  34971  bnj250  35252  bnj255  35256  bnj345  35265  bnj945  35324  bnj1209  35346  bnj1275  35363  bnj543  35443  bnj571  35456  bnj607  35466  bnj882  35476  bnj983  35501  bnj996  35506  bnj1006  35510  bnj1033  35519  bnj1097  35531  bnj1110  35532  bnj1145  35543  bnj1174  35553  bnj1189  35559  bnj1450  35600  bnj1514  35613  axprALT2  35658  wevgblacfn  35809  cusgr3cyclex  35826  erdszelem1  35871  cvmsval  35946  cvmliftiota  35981  snmlval  36011  lediv2aALT  36357  elwlim  36501  brtxp2  36559  brpprod3a  36564  brcart  36610  lemsuccf  36619  broutsideof3  36807  ivthALT  37039  df3nandALT2  37104  andnand1  37105  topdifinffinlem  38184  relowlssretop  38200  rdgeqoa  38207  unccur  38440  fin2solem  38443  poimirlem3  38455  poimirlem4  38456  poimirlem26  38478  poimirlem27  38479  poimirlem32  38484  itg2gt0cn  38507  iblabsnclem  38515  areacirc  38545  impprop  38558  neificl  38601  ablo4pnp  38728  isrngohom  38813  isidl  38862  ispridl  38882  pridlidl  38883  ismaxidl  38888  maxidlidl  38889  isfldidl2  38917  isdmn3  38922  triantru3  39082  moantr  39218  brxrn2  39230  dfxrn2  39231  ecxrn  39252  disjressuc2  39257  inxpxrn  39264  rnxrn  39267  dfsuccl4  39320  dmqsblocks  39813  islshp  39950  isopos  40151  cvrfval  40239  cvrval  40240  isatl  40270  isat3  40278  islpln5  40506  4atlem11  40580  dalem20  40664  lhpexle3  40983  lhpex2leN  40984  isltrn2N  41091  diclspsn  42165  lcfls1lem  42505  lcfls1N  42506  uzindd  42942  isprimroot  43057  flt4lem5e  43600  3cubes  43633  fz1eqin  43712  dflim6  44203  dflim7  44212  nnoeomeqom  44251  cantnfub2  44261  fzunt  44393  fzuntd  44394  fzunt1d  44395  fzuntgd  44396  rp-isfinite6  44456  snhesn  44724  ismnuprim  45216  ismnushort  45223  iotasbc2  45342  eelT00  45625  eelTTT  45626  eelT11  45627  eelT12  45629  eelTT1  45630  eelT01  45631  eel0T1  45632  uun132  45705  uun132p1  45706  un2122  45710  uunTT1  45713  uunTT1p1  45714  uunTT1p2  45715  uunT11  45716  uunT11p1  45717  uunT11p2  45718  uunT12  45719  uunT12p1  45720  uunT12p2  45721  uunT12p3  45722  uunT12p4  45723  uunT12p5  45724  uun111  45725  uun2221  45733  uun2221p1  45734  uun2221p2  45735  stoweidlem17  46943  stoweidlem34  46960  stoweidlem60  46986  ndmaovass  48192  ndmaovdistr  48193  4an21  48256  2elfz3nn0  48302  difltmodne  48334  prproropf1o  48505  fpprel  48742  clnbgredg  48854  dfvopnbgr2  48867  dfclnbgr6  48870  dfnbgr6  48871  dfsclnbgr6  48872  uhgrimprop  48906  isuspgrimlem  48909  clnbgrgrim  48948  isgrtri  48957  isubgr3stgrlem4  48983  isubgr3stgrlem7  48986  upwlksfval  49149  isupwlkg  49151  upwlkbprop  49152  2zrngnmrid  49269  isidom3  49358  lindslinindsimp2lem5  49490  i0oii  49944  io1ii  49945  sepnsepolem1  49946  isthincd2  50461  functhinc  50472  elpg  50723  alimp-no-surprise  50793