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  3503  ceqsex2v  3504  ceqsex3v  3505  ceqsex4v  3506  ceqsex6v  3507  ceqsex8v  3508  2reu5lem1  3716  2reu5lem2  3717  2reu5lem3  3718  eldifpr  4622  rexdifpr  4623  trel3  5225  2rbropap  5547  ordelord  6383  dflim2  6420  dff1o4  6830  foco2  7105  brfvopab  7473  eloprabga  7525  ndmovass  7605  ndmovdistr  7606  dflim3  7846  dflim4  7847  frxp2  8145  mpoxopovel  8221  dfsmo2  8339  dfrecs3  8364  oeeui  8593  naddasslem2  8687  ecopovtrn  8823  elixp2  8911  elixp  8914  mptelixpg  8945  dif1en  9159  ssfi  9170  sbthfilem  9195  eqinf  9458  zorn2lem7  10507  grothprim  10846  grothtsk  10847  divmulasscom  11923  muldivdir  11934  divmuldiv  11942  sup3  12199  dfnn3  12274  prime  12705  eluz2  12896  raluz2  12949  elixx1  13409  elixx3g  13413  elioo2  13441  elioo5  13458  elicc4  13468  iccneg  13527  icoshft  13528  difreicc  13539  elfz1  13568  elfz  13569  elfz2  13570  elfzm11  13652  elfz2nn0  13675  elfzo2  13719  elfzo3  13734  lbfzo0  13757  fzo1lb  13771  1elfzo1  13772  fzind2  13846  zmodid2  13962  hashgt23el  14491  swrdnd2  14727  swrdnd0  14729  swrdccatin1  14796  swrdccat  14806  repswswrd  14857  swrdco  14910  2swrd2eqwrdeq  15028  rediv  15220  imdiv  15227  cosmul  16265  bitsval  16518  bitsmod  16530  bitscmp  16532  smueqlem  16584  dfgcd2  16640  lcmneg  16697  lcmftp  16730  coprmgcdb  16743  divgcdcoprmex  16760  cncongr1  16761  cncongr2  16762  difsqpwdvds  16983  oddprmdvds  16999  elgz  17027  xpsfrnel  17652  xpsfrnel2  17654  ismre  17678  mreexexlem4d  17739  iscatd2  17773  isssc  17913  eldmcoa  18158  isdrs  18393  isipodrs  18629  mgmsscl  18739  ismhm  18894  mhmpropd  18901  issubm  18912  issubmndb  18914  submacs  18937  issubg  19250  eqglact  19305  eqgid  19306  ecqusaddd  19321  ecqusaddcl  19322  pgrpsubgsymgbi  19536  isslw  19736  efgsdm  19858  mulgmhm  19955  mulgghm  19956  dmdprd  20128  dprdw  20140  subgdmdprd  20164  dmdprdpr  20179  isomnd  20251  isrng  20290  issrg  20328  srglmhm  20361  srgrmhm  20362  isring  20377  ringlghm  20455  dfrhm2  20616  isrhm0  20618  crngrhmfo  20638  issubrng  20710  issubrg3  20763  isdomn3  20877  isdrng3  20917  issdrg  20955  sdrgacs  20968  islmod  21049  lsspropd  21202  islmhm  21212  islbs  21261  lbspropd  21284  isfieldidl  21450  isfieldidl2  21451  qusmulrng  21486  rngqiprngghmlem3  21493  rngqiprnglinlem3  21497  rngqiprnglin  21506  isprmidl  21527  isprmidlc  21536  cnfldfunALT  21601  isphl  21842  elocv  21882  isobs  21934  mat1dimscm  22698  scmatghm  22756  scmatmhm  22757  ma1repvcl  22793  smadiadetr  22898  mat2pmatghm  22956  mat2pmatmul  22957  decpmatmulsumfsupp  22999  pm2mpghm  23042  pm2mpmhmlem1  23044  neindisj  23343  lmbrf  23486  hauscmplem  23632  llyi  23701  subislly  23708  islocfin  23744  uptx  23852  txcn  23853  qtopeu  23943  elmptrab  24054  isfbas  24056  trfil2  24114  flimcls  24212  cnextcn  24294  xmetec  24661  ngppropd  24864  ngpocelbl  24931  bl2ioo  25019  xrtgioo  25034  om1elbas  25261  elpi1  25274  isclm  25293  isclmp  25326  isncvsngp  25378  iscph  25399  tcphcph  25466  lmmbr2  25488  lmmbrf  25491  iscau2  25506  caussi  25526  lmclim  25532  bcthlem1  25553  srabn  25589  ishl2  25599  evthicc2  25689  ovolfioo  25696  ovolficc  25697  iblcnlem1  26017  iblrelem  26020  iblre  26023  iblcn  26028  isuc1p  26368  ismon1p  26370  ellogrn  26794  logreclem  26997  atandm  27111  atandm2  27112  atandm3  27113  atans2  27166  dmarea  27192  dchrelbas4  27477  lgsmodeq  27576  lgsmulsqcoprm  27577  nocvxminlem  28017  cutcuts  28044  cutbday  28047  addcuts2  28242  mulcut2  28396  ax5seg  29381  eengtrkg  29429  uspgredg2v  29670  nb3grpr2  29829  isrusgr0  30012  rusgrprop0  30013  ewlkprop  30049  wksfval  30055  wlkeq  30079  wlkson  30100  wlkonprop  30102  upgr2wlk  30112  upgrtrls  30149  upgristrl  30150  wksonproplem  30152  pthsfval  30169  ispth  30171  dfpth2  30179  isspthonpth  30200  uhgrwkspth  30206  usgr2wlkspth  30210  crctcshwlkn0lem4  30267  wspthnp  30304  wwlknon  30311  wwlksnextwrd  30351  wwlksnextinj  30353  wspthsnwspthsnon  30370  umgr2adedgwlk  30399  umgr2adedgwlkon  30400  umgr2adedgwlkonALT  30401  umgr2adedgspth  30402  s3wwlks2on  30410  sps3wwlks2on  30411  wpthswwlks2on  30418  usgr2wspthons3  30421  usgr2wspthon  30422  elwwlks2  30423  elwspths2spth  30424  rusgrnumwwlkl1  30425  rusgrnumwwlkslem  30426  isclwwlk  30440  clwwlkbp  30441  clwlkclwwlklem3  30457  isclwwlknx  30492  clwwlknp  30493  clwwlkn1  30497  clwwlkn2  30500  clwwlkwwlksb  30510  clwwlknonel  30551  0pth  30581  frcond4  30736  1to3vfriswmgr  30746  3cyclfrgr  30754  frgrwopreglem5  30787  2clwwlk2clwwlk  30816  numclwlk1lem1  30835  numclwwlk6  30856  ajval  31328  issh  31675  dmadjss  32354  adjeu  32356  adjval  32357  isst  32680  ishst  32681  xrdifh  33238  nndiffz1  33244  xdivpnfrp  33365  isslmd  33629  ismxidl  33852  ressply1mon1p  33965  isrrext  34497  ismntop  34523  isros  34666  issros  34673  issibf  34831  eulerpartleme  34861  eulerpartlemt0  34867  probun  34917  bnj250  35198  bnj255  35202  bnj345  35211  bnj945  35270  bnj1209  35292  bnj1275  35309  bnj543  35389  bnj571  35402  bnj607  35412  bnj882  35422  bnj983  35447  bnj996  35452  bnj1006  35456  bnj1033  35465  bnj1097  35477  bnj1110  35478  bnj1145  35489  bnj1174  35499  bnj1189  35505  bnj1450  35546  bnj1514  35559  axprALT2  35604  wevgblacfn  35695  cusgr3cyclex  35712  erdszelem1  35757  cvmsval  35832  cvmliftiota  35867  snmlval  35897  lediv2aALT  36243  elwlim  36387  brtxp2  36445  brpprod3a  36450  brcart  36496  lemsuccf  36505  broutsideof3  36693  ivthALT  36941  df3nandALT2  37006  andnand1  37007  topdifinffinlem  38088  relowlssretop  38104  rdgeqoa  38111  unccur  38344  fin2solem  38347  poimirlem3  38359  poimirlem4  38360  poimirlem26  38382  poimirlem27  38383  poimirlem32  38388  itg2gt0cn  38411  iblabsnclem  38419  areacirc  38449  neificl  38490  ablo4pnp  38617  isrngohom  38702  isidl  38751  ispridl  38771  pridlidl  38772  ismaxidl  38777  maxidlidl  38778  isfldidl2  38806  isdmn3  38811  triantru3  38971  moantr  39107  brxrn2  39119  dfxrn2  39120  ecxrn  39141  disjressuc2  39146  inxpxrn  39153  rnxrn  39156  dfsuccl4  39209  dmqsblocks  39702  islshp  39839  isopos  40040  cvrfval  40128  cvrval  40129  isatl  40159  isat3  40167  islpln5  40395  4atlem11  40469  dalem20  40553  lhpexle3  40872  lhpex2leN  40873  isltrn2N  40980  diclspsn  42054  lcfls1lem  42394  lcfls1N  42395  uzindd  42831  isprimroot  42946  flt4lem5e  43489  3cubes  43522  fz1eqin  43601  dflim6  44092  dflim7  44101  nnoeomeqom  44140  cantnfub2  44150  fzunt  44282  fzuntd  44283  fzunt1d  44284  fzuntgd  44285  rp-isfinite6  44345  snhesn  44613  ismnuprim  45105  ismnushort  45112  iotasbc2  45231  eelT00  45514  eelTTT  45515  eelT11  45516  eelT12  45518  eelTT1  45519  eelT01  45520  eel0T1  45521  uun132  45594  uun132p1  45595  un2122  45599  uunTT1  45602  uunTT1p1  45603  uunTT1p2  45604  uunT11  45605  uunT11p1  45606  uunT11p2  45607  uunT12  45608  uunT12p1  45609  uunT12p2  45610  uunT12p3  45611  uunT12p4  45612  uunT12p5  45613  uun111  45614  uun2221  45622  uun2221p1  45623  uun2221p2  45624  stoweidlem17  46832  stoweidlem34  46849  stoweidlem60  46875  ndmaovass  48081  ndmaovdistr  48082  4an21  48145  2elfz3nn0  48191  difltmodne  48223  prproropf1o  48394  fpprel  48631  clnbgredg  48743  dfvopnbgr2  48756  dfclnbgr6  48759  dfnbgr6  48760  dfsclnbgr6  48761  uhgrimprop  48795  isuspgrimlem  48798  clnbgrgrim  48837  isgrtri  48846  isubgr3stgrlem4  48872  isubgr3stgrlem7  48875  upwlksfval  49038  isupwlkg  49040  upwlkbprop  49041  2zrngnmrid  49158  isidom3  49247  lindslinindsimp2lem5  49379  i0oii  49833  io1ii  49834  sepnsepolem1  49835  isthincd2  50350  functhinc  50361  elpg  50627  alimp-no-surprise  50697