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  13an22anass  1379  4anpull2OLD  1384  3biant1d  1510  an33rean  1515  cad1  1650  3exdistr  1995  ceqsex2  3504  ceqsex2v  3505  ceqsex3v  3506  ceqsex4v  3507  ceqsex6v  3508  ceqsex8v  3509  2reu5lem1  3716  2reu5lem2  3717  2reu5lem3  3718  eldifpr  4619  rexdifpr  4620  trel3  5224  2rbropap  5543  ordelord  6399  dflim2  6436  dff1o4  6852  foco2  7130  brfvopab  7497  eloprabga  7549  ndmovass  7630  ndmovdistr  7631  dflim3  7879  dflim4  7880  frxp2  8185  mpoxopovel  8262  dfsmo2  8380  dfrecs3  8405  oeeui  8636  naddasslem2  8730  ecopovtrn  8866  elixp2  8954  elixp  8957  mptelixpg  8988  dif1en  9202  ssfi  9213  sbthfilem  9238  eqinf  9501  zorn2lem7  10604  grothprim  10943  grothtsk  10944  divmulasscom  12022  muldivdir  12033  divmuldiv  12041  sup3  12298  dfnn3  12373  prime  12804  eluz2  12995  raluz2  13048  elixx1  13509  elixx3g  13513  elioo2  13541  elioo5  13558  elicc4  13568  iccneg  13627  icoshft  13628  difreicc  13639  elfz1  13668  elfz  13669  elfz2  13670  elfzm11  13753  elfz2nn0  13776  elfzo2  13820  elfzo3  13835  lbfzo0  13858  fzo1lb  13872  1elfzo1  13873  fzind2  13947  zmodid2  14063  hashgt23el  14593  swrdnd2  14830  swrdnd0  14832  swrdccatin1  14899  swrdccat  14909  repswswrd  14960  swrdco  15013  2swrd2eqwrdeq  15132  rediv  15324  imdiv  15331  cosmul  16367  bitsval  16620  bitsmod  16632  bitscmp  16634  smueqlem  16686  dfgcd2  16745  lcmneg  16804  lcmftp  16837  coprmgcdb  16850  divgcdcoprmex  16867  cncongr1  16868  cncongr2  16869  difsqpwdvds  17091  oddprmdvds  17107  elgz  17135  xpsfrnel  17760  xpsfrnel2  17762  ismre  17786  mreexexlem4d  17847  iscatd2  17881  isssc  18021  eldmcoa  18266  isdrs  18501  isipodrs  18737  mgmsscl  18847  ismhm  19006  mhmpropd  19013  issubm  19024  issubmndb  19026  submacs  19049  issubg  19362  eqglact  19417  eqgid  19418  ecqusaddd  19433  ecqusaddcl  19434  pgrpsubgsymgbi  19649  isslw  19849  efgsdm  19971  mulgmhm  20068  mulgghm  20069  dmdprd  20241  dprdw  20253  subgdmdprd  20277  dmdprdpr  20292  isomnd  20364  isrng  20403  issrg  20441  srglmhm  20474  srgrmhm  20475  isring  20490  dfring3  20545  ringlghm  20570  dfrhm2  20731  isrhm0  20733  crngrhmfo  20753  issubrng  20826  issubrg3  20879  isdomn3  20993  isdrng3  21034  issdrg  21072  sdrgacs  21085  islmod  21166  lsspropd  21319  islmhm  21329  islbs  21378  lbspropd  21401  isfieldidl  21567  isfieldidl2  21568  qusmulrng  21605  rngqiprngghmlem3  21612  rngqiprnglinlem3  21616  rngqiprnglin  21625  isprmidl  21646  isprmidlc  21655  cnfldfunALT  21720  isphl  21961  elocv  22001  isobs  22053  mat1dimscm  22817  scmatghm  22875  scmatmhm  22876  ma1repvcl  22912  smadiadetr  23017  mat2pmatghm  23075  mat2pmatmul  23076  decpmatmulsumfsupp  23118  pm2mpghm  23161  pm2mpmhmlem1  23163  neindisj  23462  lmbrf  23605  hauscmplem  23751  llyi  23820  subislly  23827  islocfin  23863  uptx  23971  txcn  23972  qtopeu  24062  elmptrab  24173  isfbas  24175  trfil2  24233  flimcls  24331  cnextcn  24413  xmetec  24780  ngppropd  24983  ngpocelbl  25050  bl2ioo  25138  xrtgioo  25153  om1elbas  25380  elpi1  25393  isclm  25412  isclmp  25445  isncvsngp  25497  iscph  25518  tcphcph  25585  lmmbr2  25607  lmmbrf  25610  iscau2  25625  caussi  25645  lmclim  25651  bcthlem1  25672  srabn  25708  ishl2  25718  evthicc2  25808  ovolfioo  25815  ovolficc  25816  iblcnlem1  26135  iblrelem  26138  iblre  26141  iblcn  26146  isuc1p  26486  ismon1p  26488  ellogrn  26914  logreclem  27117  atandm  27231  atandm2  27232  atandm3  27233  atans2  27286  dmarea  27312  dchrelbas4  27597  lgsmodeq  27696  lgsmulsqcoprm  27697  flt4lem5e  28013  nocvxminlem  28167  cutcuts  28194  cutbday  28197  addcuts2  28392  mulcut2  28546  ax5seg  29543  eengtrkg  29591  uspgredg2v  29832  nb3grpr2  29991  isrusgr0  30174  rusgrprop0  30175  ewlkprop  30211  wksfval  30217  wlkeq  30241  wlkson  30262  wlkonprop  30264  upgr2wlk  30274  upgrtrls  30311  upgristrl  30312  wksonproplem  30314  pthsfval  30331  ispth  30333  dfpth2  30341  isspthonpth  30362  uhgrwkspth  30368  usgr2wlkspth  30372  crctcshwlkn0lem4  30429  wspthnp  30466  wwlknon  30473  wwlksnextwrd  30513  wwlksnextinj  30515  wspthsnwspthsnon  30532  umgr2adedgwlk  30561  umgr2adedgwlkon  30562  umgr2adedgwlkonALT  30563  umgr2adedgspth  30564  s3wwlks2on  30572  sps3wwlks2on  30573  wpthswwlks2on  30580  usgr2wspthons3  30583  usgr2wspthon  30584  elwwlks2  30585  elwspths2spth  30586  rusgrnumwwlkl1  30587  rusgrnumwwlkslem  30588  isclwwlk  30602  clwwlkbp  30603  clwlkclwwlklem3  30619  isclwwlknx  30654  clwwlknp  30655  clwwlkn1  30659  clwwlkn2  30662  clwwlkwwlksb  30672  clwwlknonel  30713  0pth  30743  frcond4  30898  1to3vfriswmgr  30908  3cyclfrgr  30916  frgrwopreglem5  30949  2clwwlk2clwwlk  30978  numclwlk1lem1  30997  numclwwlk6  31018  ajval  31490  issh  31837  dmadjss  32516  adjeu  32518  adjval  32519  isst  32842  ishst  32843  xrdifh  33439  nndiffz1  33445  xdivpnfrp  33566  isslmd  33830  ismxidl  34054  ressply1mon1p  34167  isrrext  34699  ismntop  34725  isros  34868  issros  34875  issibf  35032  eulerpartleme  35062  eulerpartlemt0  35068  probun  35118  bnj250  35399  bnj255  35403  bnj345  35412  bnj945  35471  bnj1209  35493  bnj1275  35510  bnj543  35590  bnj571  35603  bnj607  35613  bnj882  35623  bnj983  35648  bnj996  35653  bnj1006  35657  bnj1033  35666  bnj1097  35678  bnj1110  35679  bnj1145  35690  bnj1174  35700  bnj1189  35706  bnj1450  35747  bnj1514  35760  axprALT2  35815  wevgblacfn  36038  cusgr3cyclex  36067  srepdflem1  36084  erdszelem1  36122  cvmsval  36197  cvmliftiota  36232  snmlval  36262  lediv2aALT  36608  mirimanofffr  36628  elwlim  36762  brtxp2  36820  brpprod3a  36825  brcart  36871  lemsuccf  36880  broutsideof3  37068  ivthALT  37300  df3nandALT2  37365  andnand1  37366  topdifinffinlem  38461  relowlssretop  38477  rdgeqoa  38484  unccur  38717  fin2solem  38720  poimirlem3  38732  poimirlem4  38733  poimirlem26  38755  poimirlem27  38756  poimirlem32  38761  itg2gt0cn  38784  iblabsnclem  38792  areacirc  38822  impprop  38835  neificl  38878  ablo4pnp  39005  isrngohom  39090  isidl  39139  ispridl  39159  pridlidl  39160  ismaxidl  39165  maxidlidl  39166  isfldidl2  39194  isdmn3  39199  triantru3  39359  moantr  39495  brxrn2  39507  dfxrn2  39508  ecxrn  39529  disjressuc2  39534  inxpxrn  39541  rnxrn  39544  dfsuccl4  39597  dmqsblocks  40090  islshp  40227  isopos  40428  cvrfval  40516  cvrval  40517  isatl  40547  isat3  40555  islpln5  40783  4atlem11  40857  dalem20  40941  lhpexle3  41260  lhpex2leN  41261  isltrn2N  41368  diclspsn  42442  lcfls1lem  42782  lcfls1N  42783  uzindd  43219  isprimroot  43334  3cubes  43891  fz1eqin  43971  dflim6  44456  dflim7  44465  nnoeomeqom  44504  cantnfub2  44514  fzunt  44646  fzuntd  44647  fzunt1d  44648  fzuntgd  44649  rp-isfinite6  44709  snhesn  44976  ismnuprim  45468  ismnushort  45475  iotasbc2  45593  eelT00  45876  eelTTT  45877  eelT11  45878  eelT12  45880  eelTT1  45881  eelT01  45882  eel0T1  45883  uun132  45956  uun132p1  45957  un2122  45961  uunTT1  45964  uunTT1p1  45965  uunTT1p2  45966  uunT11  45967  uunT11p1  45968  uunT11p2  45969  uunT12  45970  uunT12p1  45971  uunT12p2  45972  uunT12p3  45973  uunT12p4  45974  uunT12p5  45975  uun111  45976  uun2221  45984  uun2221p1  45985  uun2221p2  45986  stoweidlem17  47230  stoweidlem34  47247  stoweidlem60  47273  ndmaovass  48479  ndmaovdistr  48480  4an21  48543  2elfz3nn0  48589  difltmodne  48621  prproropf1o  48792  fpprel  49029  clnbgredg  49141  dfvopnbgr2  49154  dfclnbgr6  49157  dfnbgr6  49158  dfsclnbgr6  49159  uhgrimprop  49193  isuspgrimlem  49196  clnbgrgrim  49235  isgrtri  49244  isubgr3stgrlem4  49270  isubgr3stgrlem7  49273  upwlksfval  49436  isupwlkg  49438  upwlkbprop  49439  2zrngnmrid  49556  isidom3  49645  lindslinindsimp2lem5  49777  i0oii  50237  io1ii  50238  sepnsepolem1  50239  isnat3  50545  fucoisfunc  50690  isthincd2  50775  functhinc  50786  elpg  51085  alimp-no-surprise  51155