Theorem 3anass 1110

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 1104	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		anass 473	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3	1, 2	bitri 278	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 400   ∧ w3a 1102

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 401  df-3an 1104

This theorem is used by:  3anan12  1111  3ancoma  1114  anandi3  1118  4anpull2OLD  1382  3biant1d  1508  an33rean  1513  cad1  1646  3exdistr  1989  ceqsex2  3504  ceqsex2v  3505  ceqsex3v  3506  ceqsex4v  3507  ceqsex6v  3508  ceqsex8v  3509  2reu5lem1  3717  2reu5lem2  3718  2reu5lem3  3719  eldifpr  4623  rexdifpr  4624  trel3  5226  2rbropap  5548  ordelord  6382  dflim2  6419  dff1o4  6829  foco2  7104  brfvopab  7469  eloprabga  7521  ndmovass  7600  ndmovdistr  7601  dflim3  7841  dflim4  7842  frxp2  8138  mpoxopovel  8214  dfsmo2  8332  dfrecs3  8357  oeeui  8586  naddasslem2  8680  ecopovtrn  8816  elixp2  8897  elixp  8900  mptelixpg  8931  dif1en  9144  ssfi  9155  sbthfilem  9180  eqinf  9443  zorn2lem7  10492  grothprim  10825  grothtsk  10826  divmulasscom  11902  muldivdir  11913  divmuldiv  11921  sup3  12178  dfnn3  12253  prime  12683  eluz2  12874  raluz2  12927  elixx1  13387  elixx3g  13391  elioo2  13419  elioo5  13436  elicc4  13446  iccneg  13505  icoshft  13506  difreicc  13517  elfz1  13546  elfz  13547  elfz2  13548  elfzm11  13630  elfz2nn0  13653  elfzo2  13697  elfzo3  13712  lbfzo0  13735  fzo1lb  13749  1elfzo1  13750  fzind2  13824  zmodid2  13939  hashgt23el  14468  swrdnd2  14700  swrdnd0  14702  swrdccatin1  14769  swrdccat  14779  repswswrd  14828  swrdco  14881  2swrd2eqwrdeq  14997  rediv  15189  imdiv  15196  cosmul  16235  bitsval  16488  bitsmod  16500  bitscmp  16502  smueqlem  16554  dfgcd2  16610  lcmneg  16667  lcmftp  16700  coprmgcdb  16713  divgcdcoprmex  16730  cncongr1  16731  cncongr2  16732  difsqpwdvds  16953  oddprmdvds  16969  elgz  16997  xpsfrnel  17622  xpsfrnel2  17624  ismre  17648  mreexexlem4d  17709  iscatd2  17743  isssc  17883  eldmcoa  18128  isdrs  18363  isipodrs  18599  mgmsscl  18709  ismhm  18849  mhmpropd  18856  issubm  18867  issubmndb  18869  submacs  18892  issubg  19198  eqglact  19253  eqgid  19254  ecqusaddd  19269  ecqusaddcl  19270  pgrpsubgsymgbi  19484  isslw  19684  efgsdm  19806  mulgmhm  19903  mulgghm  19904  dmdprd  20076  dprdw  20088  subgdmdprd  20112  dmdprdpr  20127  isomnd  20199  isrng  20238  issrg  20276  srglmhm  20309  srgrmhm  20310  isring  20325  ringlghm  20402  dfrhm2  20563  isrhm0  20565  crngrhmfo  20585  issubrng  20657  issubrg3  20710  isdomn3  20824  isdrng3  20864  issdrg  20902  sdrgacs  20915  islmod  20996  lsspropd  21149  islmhm  21159  islbs  21208  lbspropd  21231  isfieldidl  21397  isfieldidl2  21398  qusmulrng  21433  rngqiprngghmlem3  21440  rngqiprnglinlem3  21444  rngqiprnglin  21453  isprmidl  21474  isprmidlc  21483  cnfldfunALT  21548  isphl  21789  elocv  21829  isobs  21881  mat1dimscm  22643  scmatghm  22701  scmatmhm  22702  ma1repvcl  22738  smadiadetr  22843  mat2pmatghm  22898  mat2pmatmul  22899  decpmatmulsumfsupp  22941  pm2mpghm  22984  pm2mpmhmlem1  22986  neindisj  23285  lmbrf  23428  hauscmplem  23574  llyi  23642  subislly  23649  islocfin  23685  uptx  23793  txcn  23794  qtopeu  23884  elmptrab  23995  isfbas  23997  trfil2  24055  flimcls  24153  cnextcn  24235  xmetec  24602  ngppropd  24805  ngpocelbl  24872  bl2ioo  24960  xrtgioo  24975  om1elbas  25202  elpi1  25215  isclm  25234  isclmp  25267  isncvsngp  25319  iscph  25340  tcphcph  25407  lmmbr2  25429  lmmbrf  25432  iscau2  25447  caussi  25467  lmclim  25473  bcthlem1  25494  srabn  25530  ishl2  25540  evthicc2  25630  ovolfioo  25637  ovolficc  25638  iblcnlem1  25958  iblrelem  25961  iblre  25964  iblcn  25969  isuc1p  26309  ismon1p  26311  ellogrn  26735  logreclem  26938  atandm  27052  atandm2  27053  atandm3  27054  atans2  27107  dmarea  27133  dchrelbas4  27418  lgsmodeq  27517  lgsmulsqcoprm  27518  nocvxminlem  27958  cutcuts  27985  cutbday  27988  addcuts2  28183  mulcut2  28337  ax5seg  29299  eengtrkg  29347  uspgredg2v  29585  nb3grpr2  29744  isrusgr0  29927  rusgrprop0  29928  ewlkprop  29964  wksfval  29970  wlkeq  29994  wlkson  30015  wlkonprop  30017  upgr2wlk  30027  upgrtrls  30060  upgristrl  30061  wksonproplem  30063  pthsfval  30079  ispth  30081  dfpth2  30089  isspthonpth  30109  uhgrwkspth  30115  usgr2wlkspth  30119  crctcshwlkn0lem4  30173  wspthnp  30210  wwlknon  30217  wwlksnextwrd  30257  wwlksnextinj  30259  wspthsnwspthsnon  30276  umgr2adedgwlk  30305  umgr2adedgwlkon  30306  umgr2adedgwlkonALT  30307  umgr2adedgspth  30308  s3wwlks2on  30316  sps3wwlks2on  30317  wpthswwlks2on  30324  usgr2wspthons3  30327  usgr2wspthon  30328  elwwlks2  30329  elwspths2spth  30330  rusgrnumwwlkl1  30331  rusgrnumwwlkslem  30332  isclwwlk  30346  clwwlkbp  30347  clwlkclwwlklem3  30363  isclwwlknx  30398  clwwlknp  30399  clwwlkn1  30403  clwwlkn2  30406  clwwlkwwlksb  30416  clwwlknonel  30457  0pth  30487  frcond4  30632  1to3vfriswmgr  30642  3cyclfrgr  30650  frgrwopreglem5  30683  2clwwlk2clwwlk  30712  numclwlk1lem1  30731  numclwwlk6  30752  ajval  31224  issh  31571  dmadjss  32250  adjeu  32252  adjval  32253  isst  32576  ishst  32577  xrdifh  33136  nndiffz1  33142  xdivpnfrp  33263  isslmd  33531  ismxidl  33754  ressply1mon1p  33867  isrrext  34399  ismntop  34425  isros  34567  issros  34574  issibf  34732  eulerpartleme  34762  eulerpartlemt0  34768  probun  34818  bnj250  35099  bnj255  35103  bnj345  35112  bnj945  35171  bnj1209  35193  bnj1275  35210  bnj543  35290  bnj571  35303  bnj607  35313  bnj882  35323  bnj983  35348  bnj996  35353  bnj1006  35357  bnj1033  35366  bnj1097  35378  bnj1110  35379  bnj1145  35390  bnj1174  35400  bnj1189  35406  bnj1450  35447  bnj1514  35460  axprALT2  35512  wevgblacfn  35603  cusgr3cyclex  35636  erdszelem1  35691  cvmsval  35766  cvmliftiota  35801  snmlval  35831  lediv2aALT  36177  elwlim  36321  brtxp2  36379  brpprod3a  36384  brcart  36430  lemsuccf  36439  broutsideof3  36626  ivthALT  36874  df3nandALT2  36939  andnand1  36940  topdifinffinlem  38021  relowlssretop  38037  rdgeqoa  38044  unccur  38282  fin2solem  38285  poimirlem3  38302  poimirlem4  38303  poimirlem26  38325  poimirlem27  38326  poimirlem32  38331  itg2gt0cn  38354  iblabsnclem  38362  areacirc  38392  neificl  38432  ablo4pnp  38559  isrngohom  38644  isidl  38693  ispridl  38713  pridlidl  38714  ismaxidl  38719  maxidlidl  38720  isfldidl2  38748  isdmn3  38753  triantru3  38913  moantr  39049  brxrn2  39061  dfxrn2  39062  ecxrn  39083  disjressuc2  39088  inxpxrn  39095  rnxrn  39098  dfsuccl4  39151  dmqsblocks  39644  islshp  39781  isopos  39982  cvrfval  40070  cvrval  40071  isatl  40101  isat3  40109  islpln5  40337  4atlem11  40411  dalem20  40495  lhpexle3  40814  lhpex2leN  40815  isltrn2N  40922  diclspsn  41996  lcfls1lem  42336  lcfls1N  42337  uzindd  42773  isprimroot  42888  flt4lem5e  43416  3cubes  43449  fz1eqin  43528  dflim6  44019  dflim7  44028  nnoeomeqom  44067  cantnfub2  44077  fzunt  44209  fzuntd  44210  fzunt1d  44211  fzuntgd  44212  rp-isfinite6  44272  snhesn  44540  ismnuprim  45032  ismnushort  45039  iotasbc2  45158  eelT00  45441  eelTTT  45442  eelT11  45443  eelT12  45445  eelTT1  45446  eelT01  45447  eel0T1  45448  uun132  45521  uun132p1  45522  un2122  45526  uunTT1  45529  uunTT1p1  45530  uunTT1p2  45531  uunT11  45532  uunT11p1  45533  uunT11p2  45534  uunT12  45535  uunT12p1  45536  uunT12p2  45537  uunT12p3  45538  uunT12p4  45539  uunT12p5  45540  uun111  45541  uun2221  45549  uun2221p1  45550  uun2221p2  45551  stoweidlem17  46759  stoweidlem34  46776  stoweidlem60  46802  ndmaovass  47971  ndmaovdistr  47972  4an21  48035  2elfz3nn0  48081  difltmodne  48113  prproropf1o  48284  fpprel  48521  clnbgredg  48633  dfvopnbgr2  48646  dfclnbgr6  48649  dfnbgr6  48650  dfsclnbgr6  48651  uhgrimprop  48685  isuspgrimlem  48688  clnbgrgrim  48727  isgrtri  48736  isubgr3stgrlem4  48762  isubgr3stgrlem7  48765  upwlksfval  48928  isupwlkg  48930  upwlkbprop  48931  2zrngnmrid  49049  isidom3  49138  lindslinindsimp2lem5  49270  i0oii  49726  io1ii  49727  sepnsepolem1  49728  isthincd2  50243  functhinc  50254  elpg  50520  alimp-no-surprise  50587