Theorem 3anass 1095

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 1089	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		anass 468	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3	1, 2	bitri 275	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3anan12  1096  3ancoma  1098  anandi3  1102  4anpull2  1363  3biant1d  1481  an33rean  1486  cad1  1619  3exdistr  1962  ceqsex2  3494  ceqsex2v  3495  ceqsex3v  3496  ceqsex4v  3497  ceqsex6v  3498  ceqsex8v  3499  2reu5lem1  3714  2reu5lem2  3715  2reu5lem3  3716  eldifpr  4616  rexdifpr  4617  trel3  5215  2rbropap  5513  ordelord  6340  dflim2  6376  dff1o4  6783  foco2  7056  brfvopab  7417  eloprabga  7469  ndmovass  7548  ndmovdistr  7549  dflim3  7791  dflim4  7792  frxp2  8088  mpoxopovel  8164  dfsmo2  8281  dfrecs3  8306  oeeui  8532  naddasslem2  8625  ecopovtrn  8761  elixp2  8843  elixp  8846  mptelixpg  8877  dif1en  9090  ssfi  9101  sbthfilem  9126  eqinf  9392  zorn2lem7  10416  grothprim  10749  grothtsk  10750  divmulasscom  11824  muldivdir  11838  divmuldiv  11845  sup3  12103  dfnn3  12163  prime  12577  eluz2  12761  raluz2  12814  elixx1  13274  elixx3g  13278  elioo2  13306  elioo5  13323  elicc4  13333  iccneg  13392  icoshft  13393  difreicc  13404  elfz1  13432  elfz  13433  elfz2  13434  elfzm11  13515  elfz2nn0  13538  elfzo2  13582  elfzo3  13596  lbfzo0  13619  fzo1lb  13633  1elfzo1  13634  fzind2  13708  zmodid2  13823  hashgt23el  14351  swrdnd2  14583  swrdnd0  14585  swrdccatin1  14652  swrdccat  14662  repswswrd  14711  swrdco  14764  2swrd2eqwrdeq  14880  rediv  15058  imdiv  15065  cosmul  16102  bitsval  16355  bitsmod  16367  bitscmp  16369  smueqlem  16421  dfgcd2  16477  lcmneg  16534  lcmftp  16567  coprmgcdb  16580  divgcdcoprmex  16597  cncongr1  16598  cncongr2  16599  difsqpwdvds  16819  oddprmdvds  16835  elgz  16863  xpsfrnel  17487  xpsfrnel2  17489  ismre  17513  mreexexlem4d  17574  iscatd2  17608  isssc  17748  eldmcoa  17993  isdrs  18228  isipodrs  18464  mgmsscl  18574  ismhm  18714  mhmpropd  18721  issubm  18732  issubmndb  18734  submacs  18756  issubg  19060  eqglact  19112  eqgid  19113  ecqusaddd  19125  ecqusaddcl  19126  pgrpsubgsymgbi  19341  isslw  19541  efgsdm  19663  mulgmhm  19760  mulgghm  19761  dmdprd  19933  dprdw  19945  subgdmdprd  19969  dmdprdpr  19984  isomnd  20056  isrng  20093  issrg  20127  srglmhm  20160  srgrmhm  20161  isring  20176  ringlghm  20251  dfrhm2  20414  issubrng  20484  issubrg3  20537  isdomn3  20652  issdrg  20725  sdrgacs  20738  islmod  20819  lsspropd  20973  islmhm  20983  islbs  21032  lbspropd  21055  qusmulrng  21241  rngqiprngghmlem3  21248  rngqiprnglinlem3  21252  rngqiprnglin  21261  cnfldfunALT  21328  cnfldfunALTOLD  21341  isphl  21587  elocv  21627  isobs  21679  mat1dimscm  22423  scmatghm  22481  scmatmhm  22482  ma1repvcl  22518  smadiadetr  22623  mat2pmatghm  22678  mat2pmatmul  22679  decpmatmulsumfsupp  22721  pm2mpghm  22764  pm2mpmhmlem1  22766  neindisj  23065  lmbrf  23208  hauscmplem  23354  llyi  23422  subislly  23429  islocfin  23465  uptx  23573  txcn  23574  qtopeu  23664  elmptrab  23775  isfbas  23777  trfil2  23835  flimcls  23933  cnextcn  24015  xmetec  24382  ngppropd  24585  ngpocelbl  24652  bl2ioo  24740  xrtgioo  24755  om1elbas  24992  elpi1  25005  isclm  25024  isclmp  25057  isncvsngp  25109  iscph  25130  tcphcph  25197  lmmbr2  25219  lmmbrf  25222  iscau2  25237  caussi  25257  lmclim  25263  bcthlem1  25284  srabn  25320  ishl2  25330  evthicc2  25421  ovolfioo  25428  ovolficc  25429  iblcnlem1  25749  iblrelem  25752  iblre  25755  iblcn  25760  isuc1p  26106  ismon1p  26108  ellogrn  26528  logreclem  26732  atandm  26846  atandm2  26847  atandm3  26848  atans2  26901  dmarea  26927  dchrelbas4  27214  lgsmodeq  27313  lgsmulsqcoprm  27314  nocvxminlem  27754  cutcuts  27781  cutbday  27784  addcuts2  27979  mulcut2  28133  ax5seg  29015  eengtrkg  29063  uspgredg2v  29301  nb3grpr2  29460  isrusgr0  29644  rusgrprop0  29645  ewlkprop  29681  wksfval  29687  wlkeq  29711  wlkson  29732  wlkonprop  29734  upgr2wlk  29744  upgrtrls  29777  upgristrl  29778  wksonproplem  29780  pthsfval  29796  ispth  29798  dfpth2  29806  isspthonpth  29826  uhgrwkspth  29832  usgr2wlkspth  29836  crctcshwlkn0lem4  29890  wspthnp  29927  wwlknon  29934  wwlksnextwrd  29974  wwlksnextinj  29976  wspthsnwspthsnon  29993  umgr2adedgwlk  30022  umgr2adedgwlkon  30023  umgr2adedgwlkonALT  30024  umgr2adedgspth  30025  s3wwlks2on  30033  sps3wwlks2on  30034  wpthswwlks2on  30041  usgr2wspthons3  30044  usgr2wspthon  30045  elwwlks2  30046  elwspths2spth  30047  rusgrnumwwlkl1  30048  rusgrnumwwlkslem  30049  isclwwlk  30063  clwwlkbp  30064  clwlkclwwlklem3  30080  isclwwlknx  30115  clwwlknp  30116  clwwlkn1  30120  clwwlkn2  30123  clwwlkwwlksb  30133  clwwlknonel  30174  0pth  30204  frcond4  30349  1to3vfriswmgr  30359  3cyclfrgr  30367  frgrwopreglem5  30400  2clwwlk2clwwlk  30429  numclwlk1lem1  30448  numclwwlk6  30469  ajval  30940  issh  31287  dmadjss  31966  adjeu  31968  adjval  31969  isst  32292  ishst  32293  xrdifh  32862  nndiffz1  32868  xdivpnfrp  33016  isslmd  33286  isprmidl  33521  isprmidlc  33530  ismxidl  33545  ressply1mon1p  33651  isrrext  34159  ismntop  34185  isros  34327  issros  34334  issibf  34492  eulerpartleme  34522  eulerpartlemt0  34528  probun  34578  bnj250  34859  bnj255  34863  bnj345  34872  bnj945  34931  bnj1209  34954  bnj1275  34971  bnj543  35051  bnj571  35064  bnj607  35074  bnj882  35084  bnj983  35109  bnj996  35114  bnj1006  35118  bnj1033  35127  bnj1097  35139  bnj1110  35140  bnj1145  35151  bnj1174  35161  bnj1189  35167  bnj1450  35208  bnj1514  35221  wevgblacfn  35305  cusgr3cyclex  35332  erdszelem1  35387  cvmsval  35462  cvmliftiota  35497  snmlval  35527  lediv2aALT  35873  elwlim  36017  brtxp2  36075  brpprod3a  36080  brcart  36126  lemsuccf  36135  broutsideof3  36322  ivthALT  36531  df3nandALT2  36596  andnand1  36597  topdifinffinlem  37554  relowlssretop  37570  rdgeqoa  37577  unccur  37806  fin2solem  37809  poimirlem3  37826  poimirlem4  37827  poimirlem26  37849  poimirlem27  37850  poimirlem32  37855  itg2gt0cn  37878  iblabsnclem  37886  areacirc  37916  neificl  37956  ablo4pnp  38083  isrngohom  38168  isidl  38217  ispridl  38237  pridlidl  38238  ismaxidl  38243  maxidlidl  38244  isfldidl2  38272  isdmn3  38277  triantru3  38439  moantr  38575  brxrn2  38587  dfxrn2  38588  ecxrn  38609  disjressuc2  38614  inxpxrn  38621  rnxrn  38624  dfsuccl4  38677  dmqsblocks  39170  islshp  39307  isopos  39508  cvrfval  39596  cvrval  39597  isatl  39627  isat3  39635  islpln5  39863  4atlem11  39937  dalem20  40021  lhpexle3  40340  lhpex2leN  40341  isltrn2N  40448  diclspsn  41522  lcfls1lem  41862  lcfls1N  41863  uzindd  42299  isprimroot  42415  flt4lem5e  42966  3cubes  42999  fz1eqin  43078  dflim6  43573  dflim7  43582  nnoeomeqom  43621  cantnfub2  43631  fzunt  43763  fzuntd  43764  fzunt1d  43765  fzuntgd  43766  rp-isfinite6  43826  snhesn  44094  ismnuprim  44602  ismnushort  44609  iotasbc2  44728  eelT00  45012  eelTTT  45013  eelT11  45014  eelT12  45016  eelTT1  45017  eelT01  45018  eel0T1  45019  uun132  45092  uun132p1  45093  un2122  45097  uunTT1  45100  uunTT1p1  45101  uunTT1p2  45102  uunT11  45103  uunT11p1  45104  uunT11p2  45105  uunT12  45106  uunT12p1  45107  uunT12p2  45108  uunT12p3  45109  uunT12p4  45110  uunT12p5  45111  uun111  45112  uun2221  45120  uun2221p1  45121  uun2221p2  45122  stoweidlem17  46328  stoweidlem34  46345  stoweidlem60  46371  ndmaovass  47519  ndmaovdistr  47520  4an21  47583  2elfz3nn0  47629  difltmodne  47655  prproropf1o  47820  fpprel  48041  clnbgredg  48153  dfvopnbgr2  48166  dfclnbgr6  48169  dfnbgr6  48170  dfsclnbgr6  48171  uhgrimprop  48205  isuspgrimlem  48208  clnbgrgrim  48247  isgrtri  48256  isubgr3stgrlem4  48282  isubgr3stgrlem7  48285  upwlksfval  48448  isupwlkg  48450  upwlkbprop  48451  2zrngnmrid  48569  lindslinindsimp2lem5  48775  i0oii  49232  io1ii  49233  sepnsepolem1  49234  isthincd2  49749  functhinc  49760  elpg  50026  alimp-no-surprise  50093