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  1362  3biant1d  1480  an33rean  1485  cad1  1617  3exdistr  1960  ceqsex2  3535  ceqsex2v  3536  ceqsex3v  3537  ceqsex4v  3538  ceqsex6v  3539  ceqsex8v  3540  2reu5lem1  3761  2reu5lem2  3762  2reu5lem3  3763  eldifpr  4658  rexdifpr  4659  trel3  5269  2rbropap  5571  ordelord  6406  dflim2  6441  dff1o4  6856  foco2  7129  brfvopab  7490  eloprabga  7542  ndmovass  7621  ndmovdistr  7622  dflim3  7868  dflim4  7869  frxp2  8169  mpoxopovel  8245  dfsmo2  8387  dfrecs3  8412  dfrecs3OLD  8413  oeeui  8640  naddasslem2  8733  ecopovtrn  8860  elixp2  8941  elixp  8944  mptelixpg  8975  dif1en  9200  dif1enOLD  9202  ssfi  9213  sbthfilem  9238  eqinf  9524  zorn2lem7  10542  grothprim  10874  grothtsk  10875  divmulasscom  11946  muldivdir  11960  divmuldiv  11967  sup3  12225  dfnn3  12280  prime  12699  eluz2  12884  raluz2  12939  elixx1  13396  elixx3g  13400  elioo2  13428  elioo5  13444  elicc4  13454  iccneg  13512  icoshft  13513  difreicc  13524  elfz1  13552  elfz  13553  elfz2  13554  elfzm11  13635  elfz2nn0  13658  elfzo2  13702  elfzo3  13716  lbfzo0  13739  fzo1lb  13753  fzind2  13824  zmodid2  13939  hashgt23el  14463  swrdnd2  14693  swrdnd0  14695  swrdccatin1  14763  swrdccat  14773  repswswrd  14822  swrdco  14876  2swrd2eqwrdeq  14992  rediv  15170  imdiv  15177  cosmul  16209  bitsval  16461  bitsmod  16473  bitscmp  16475  smueqlem  16527  dfgcd2  16583  lcmneg  16640  lcmftp  16673  coprmgcdb  16686  divgcdcoprmex  16703  cncongr1  16704  cncongr2  16705  difsqpwdvds  16925  oddprmdvds  16941  elgz  16969  xpsfrnel  17607  xpsfrnel2  17609  ismre  17633  mreexexlem4d  17690  iscatd2  17724  isssc  17864  eldmcoa  18110  isdrs  18347  isipodrs  18582  mgmsscl  18658  ismhm  18798  mhmpropd  18805  issubm  18816  issubmndb  18818  submacs  18840  issubg  19144  eqglact  19197  eqgid  19198  ecqusaddd  19210  ecqusaddcl  19211  pgrpsubgsymgbi  19426  isslw  19626  efgsdm  19748  mulgmhm  19845  mulgghm  19846  dmdprd  20018  dprdw  20030  subgdmdprd  20054  dmdprdpr  20069  isrng  20151  issrg  20185  srglmhm  20218  srgrmhm  20219  isring  20234  ringlghm  20309  dfrhm2  20474  issubrng  20547  issubrg3  20600  isdomn3  20715  issdrg  20789  sdrgacs  20802  islmod  20862  lsspropd  21016  islmhm  21026  islbs  21075  lbspropd  21098  qusmulrng  21292  rngqiprngghmlem3  21299  rngqiprnglinlem3  21303  rngqiprnglin  21312  cnfldfunALT  21379  cnfldfunALTOLD  21392  isphl  21646  elocv  21686  isobs  21740  mat1dimscm  22481  scmatghm  22539  scmatmhm  22540  ma1repvcl  22576  smadiadetr  22681  mat2pmatghm  22736  mat2pmatmul  22737  decpmatmulsumfsupp  22779  pm2mpghm  22822  pm2mpmhmlem1  22824  neindisj  23125  lmbrf  23268  hauscmplem  23414  llyi  23482  subislly  23489  islocfin  23525  uptx  23633  txcn  23634  qtopeu  23724  elmptrab  23835  isfbas  23837  trfil2  23895  flimcls  23993  cnextcn  24075  xmetec  24444  ngppropd  24650  ngpocelbl  24725  bl2ioo  24813  xrtgioo  24828  om1elbas  25065  elpi1  25078  isclm  25097  isclmp  25130  isncvsngp  25183  iscph  25204  tcphcph  25271  lmmbr2  25293  lmmbrf  25296  iscau2  25311  caussi  25331  lmclim  25337  bcthlem1  25358  srabn  25394  ishl2  25404  evthicc2  25495  ovolfioo  25502  ovolficc  25503  iblcnlem1  25823  iblrelem  25826  iblre  25829  iblcn  25834  isuc1p  26180  ismon1p  26182  ellogrn  26601  logreclem  26805  atandm  26919  atandm2  26920  atandm3  26921  atans2  26974  dmarea  27000  dchrelbas4  27287  lgsmodeq  27386  lgsmulsqcoprm  27387  nocvxminlem  27822  scutcut  27846  scutbday  27849  addscut2  28012  mulscut2  28159  ax5seg  28953  eengtrkg  29001  uspgredg2v  29241  nb3grpr2  29400  isrusgr0  29584  rusgrprop0  29585  ewlkprop  29621  wksfval  29627  wlkeq  29652  wlkson  29674  wlkonprop  29676  upgr2wlk  29686  upgrtrls  29719  upgristrl  29720  wksonproplem  29722  wksonproplemOLD  29723  pthsfval  29739  ispth  29741  dfpth2  29749  isspthonpth  29769  uhgrwkspth  29775  usgr2wlkspth  29779  crctcshwlkn0lem4  29833  wspthnp  29870  wwlknon  29877  wwlksnextwrd  29917  wwlksnextinj  29919  wspthsnwspthsnon  29936  umgr2adedgwlk  29965  umgr2adedgwlkon  29966  umgr2adedgwlkonALT  29967  umgr2adedgspth  29968  s3wwlks2on  29976  wpthswwlks2on  29981  usgr2wspthons3  29984  usgr2wspthon  29985  elwwlks2  29986  elwspths2spth  29987  rusgrnumwwlkl1  29988  rusgrnumwwlkslem  29989  isclwwlk  30003  clwwlkbp  30004  clwlkclwwlklem3  30020  isclwwlknx  30055  clwwlknp  30056  clwwlkn1  30060  clwwlkn2  30063  clwwlkwwlksb  30073  clwwlknonel  30114  0pth  30144  frcond4  30289  1to3vfriswmgr  30299  3cyclfrgr  30307  frgrwopreglem5  30340  2clwwlk2clwwlk  30369  numclwlk1lem1  30388  numclwwlk6  30409  ajval  30880  issh  31227  dmadjss  31906  adjeu  31908  adjval  31909  isst  32232  ishst  32233  xrdifh  32782  nndiffz1  32788  xdivpnfrp  32915  isomnd  33078  isslmd  33208  isprmidl  33466  isprmidlc  33475  ismxidl  33490  ressply1mon1p  33593  isrrext  34001  ismntop  34027  isros  34169  issros  34176  issibf  34335  eulerpartleme  34365  eulerpartlemt0  34371  probun  34421  bnj250  34715  bnj255  34719  bnj345  34728  bnj945  34787  bnj1209  34810  bnj1275  34827  bnj543  34907  bnj571  34920  bnj607  34930  bnj882  34940  bnj983  34965  bnj996  34970  bnj1006  34974  bnj1033  34983  bnj1097  34995  bnj1110  34996  bnj1145  35007  bnj1174  35017  bnj1189  35023  bnj1450  35064  bnj1514  35077  wevgblacfn  35114  cusgr3cyclex  35141  erdszelem1  35196  cvmsval  35271  cvmliftiota  35306  snmlval  35336  lediv2aALT  35682  elwlim  35824  brtxp2  35882  brpprod3a  35887  brcart  35933  brsuccf  35942  broutsideof3  36127  ivthALT  36336  df3nandALT2  36401  andnand1  36402  topdifinffinlem  37348  relowlssretop  37364  rdgeqoa  37371  unccur  37610  fin2solem  37613  poimirlem3  37630  poimirlem4  37631  poimirlem26  37653  poimirlem27  37654  poimirlem32  37659  itg2gt0cn  37682  iblabsnclem  37690  areacirc  37720  neificl  37760  ablo4pnp  37887  isrngohom  37972  isidl  38021  ispridl  38041  pridlidl  38042  ismaxidl  38047  maxidlidl  38048  isfldidl2  38076  isdmn3  38081  triantru3  38231  moantr  38365  brxrn2  38376  dfxrn2  38377  ecxrn  38388  disjressuc2  38389  inxpxrn  38396  rnxrn  38399  islshp  38980  isopos  39181  cvrfval  39269  cvrval  39270  isatl  39300  isat3  39308  islpln5  39537  4atlem11  39611  dalem20  39695  lhpexle3  40014  lhpex2leN  40015  isltrn2N  40122  diclspsn  41196  lcfls1lem  41536  lcfls1N  41537  uzindd  41978  isprimroot  42094  flt4lem5e  42666  3cubes  42701  fz1eqin  42780  dflim6  43277  dflim7  43286  nnoeomeqom  43325  cantnfub2  43335  fzunt  43468  fzuntd  43469  fzunt1d  43470  fzuntgd  43471  rp-isfinite6  43531  snhesn  43799  ismnuprim  44313  ismnushort  44320  iotasbc2  44439  eelT00  44725  eelTTT  44726  eelT11  44727  eelT12  44729  eelTT1  44730  eelT01  44731  eel0T1  44732  uun132  44805  uun132p1  44806  un2122  44810  uunTT1  44813  uunTT1p1  44814  uunTT1p2  44815  uunT11  44816  uunT11p1  44817  uunT11p2  44818  uunT12  44819  uunT12p1  44820  uunT12p2  44821  uunT12p3  44822  uunT12p4  44823  uunT12p5  44824  uun111  44825  uun2221  44833  uun2221p1  44834  uun2221p2  44835  stoweidlem17  46032  stoweidlem34  46049  stoweidlem60  46075  ndmaovass  47218  ndmaovdistr  47219  4an21  47282  2elfz3nn0  47328  difltmodne  47344  prproropf1o  47494  fpprel  47715  clnbgredg  47826  dfvopnbgr2  47839  dfclnbgr6  47842  dfnbgr6  47843  dfsclnbgr6  47844  uspgrimprop  47873  isuspgrimlem  47874  clnbgrgrim  47902  isgrtri  47910  isubgr3stgrlem4  47936  isubgr3stgrlem7  47939  upwlksfval  48051  isupwlkg  48053  upwlkbprop  48054  2zrngnmrid  48172  lindslinindsimp2lem5  48379  i0oii  48817  io1ii  48818  sepnsepolem1  48819  isthincd2  49086  functhinc  49097  elpg  49233  alimp-no-surprise  49300