Theorem 3anass 1094

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 1088	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		anass 469	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3	1, 2	bitri 274	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

Syntax hints:   ↔ wb 205   ∧ wa 396   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3anan12  1095  3ancoma  1097  anandi3  1101  3biant1d  1477  an33rean  1482  an33reanOLD  1483  cad1  1619  3exdistr  1965  ceqsex2  3483  ceqsex2v  3484  ceqsex3v  3485  ceqsex4v  3486  ceqsex6v  3487  ceqsex8v  3488  2reu5lem1  3691  2reu5lem2  3692  2reu5lem3  3693  eldifpr  4594  rexdifpr  4595  trel3  5200  2rbropap  5480  ordelord  6292  dflim2  6326  dff1o4  6733  foco2  6992  brfvopab  7341  eloprabga  7391  ndmovass  7469  ndmovdistr  7470  dflim3  7703  dflim4  7704  mpoxopovel  8045  dfsmo2  8187  dfrecs3  8212  dfrecs3OLD  8213  oeeui  8442  ecopovtrn  8618  elixp2  8698  elixp  8701  mptelixpg  8732  dif1en  8954  ssfi  8965  sbthfilem  8993  eqinf  9252  zorn2lem7  10267  grothprim  10599  grothtsk  10600  divmulasscom  11666  muldivdir  11677  divmuldiv  11684  sup3  11941  dfnn3  11996  prime  12410  eluz2  12597  raluz2  12646  elixx1  13097  elixx3g  13101  elioo2  13129  elioo5  13145  elicc4  13155  iccneg  13213  icoshft  13214  difreicc  13225  elfz1  13253  elfz  13254  elfz2  13255  elfzm11  13336  elfz2nn0  13356  elfzo2  13399  elfzo3  13413  lbfzo0  13436  fzind2  13514  zmodid2  13628  hashgt23el  14148  swrdnd2  14377  swrdnd0  14379  swrdccatin1  14447  swrdccat  14457  repswswrd  14506  swrdco  14559  2swrd2eqwrdeq  14675  ccat2s1fvwALTOLD  14679  rediv  14851  imdiv  14858  cosmul  15891  bitsval  16140  bitsmod  16152  bitscmp  16154  smueqlem  16206  dfgcd2  16263  lcmneg  16317  lcmftp  16350  coprmgcdb  16363  divgcdcoprmex  16380  cncongr1  16381  cncongr2  16382  difsqpwdvds  16597  oddprmdvds  16613  elgz  16641  xpsfrnel  17282  xpsfrnel2  17284  ismre  17308  mreexexlem4d  17365  iscatd2  17399  isssc  17541  eldmcoa  17789  isdrs  18028  isipodrs  18264  mgmsscl  18340  ismhm  18441  mhmpropd  18445  issubm  18451  issubmndb  18453  submacs  18474  issubg  18764  eqglact  18816  eqgid  18817  pgrpsubgsymgbi  19025  isslw  19222  efgsdm  19345  mulgmhm  19438  mulgghm  19439  dmdprd  19610  dprdw  19622  subgdmdprd  19646  dmdprdpr  19661  issrg  19752  srglmhm  19780  srgrmhm  19781  isring  19796  ringlghm  19852  dfrhm2  19970  issubrg3  20061  issdrg  20072  sdrgacs  20078  islmod  20136  lsspropd  20288  islmhm  20298  islbs  20347  lbspropd  20370  cnfldfunALT  20619  isphl  20842  elocv  20882  isobs  20936  mat1dimscm  21633  scmatghm  21691  scmatmhm  21692  ma1repvcl  21728  smadiadetr  21833  mat2pmatghm  21888  mat2pmatmul  21889  decpmatmulsumfsupp  21931  pm2mpghm  21974  pm2mpmhmlem1  21976  neindisj  22277  lmbrf  22420  hauscmplem  22566  llyi  22634  subislly  22641  islocfin  22677  uptx  22785  txcn  22786  qtopeu  22876  elmptrab  22987  isfbas  22989  trfil2  23047  flimcls  23145  cnextcn  23227  xmetec  23596  ngppropd  23802  ngpocelbl  23877  bl2ioo  23964  xrtgioo  23978  om1elbas  24204  elpi1  24217  isclm  24236  isclmp  24269  isncvsngp  24322  iscph  24343  tcphcph  24410  lmmbr2  24432  lmmbrf  24435  iscau2  24450  caussi  24470  lmclim  24476  bcthlem1  24497  srabn  24533  ishl2  24543  evthicc2  24633  ovolfioo  24640  ovolficc  24641  iblcnlem1  24961  iblrelem  24964  iblre  24967  iblcn  24972  isuc1p  25314  ismon1p  25316  ellogrn  25724  logreclem  25921  atandm  26035  atandm2  26036  atandm3  26037  atans2  26090  dmarea  26116  dchrelbas4  26400  lgsmodeq  26499  lgsmulsqcoprm  26500  ax5seg  27315  eengtrkg  27363  uspgredg2v  27600  nb3grpr2  27759  isrusgr0  27942  rusgrprop0  27943  ewlkprop  27979  wksfval  27985  wlkeq  28010  wlkson  28033  wlkonprop  28035  upgr2wlk  28045  upgrtrls  28078  upgristrl  28079  wksonproplem  28081  wksonproplemOLD  28082  pthsfval  28098  ispth  28100  isspthonpth  28126  uhgrwkspth  28132  usgr2wlkspth  28136  crctcshwlkn0lem4  28187  wspthnp  28224  wwlknon  28231  wwlksnextwrd  28271  wwlksnextinj  28273  wspthsnwspthsnon  28290  umgr2adedgwlk  28319  umgr2adedgwlkon  28320  umgr2adedgwlkonALT  28321  umgr2adedgspth  28322  s3wwlks2on  28330  wpthswwlks2on  28335  usgr2wspthons3  28338  usgr2wspthon  28339  elwwlks2  28340  elwspths2spth  28341  rusgrnumwwlkl1  28342  rusgrnumwwlkslem  28343  isclwwlk  28357  clwwlkbp  28358  clwlkclwwlklem3  28374  isclwwlknx  28409  clwwlknp  28410  clwwlkn1  28414  clwwlkn2  28417  clwwlkwwlksb  28427  clwwlknonel  28468  0pth  28498  frcond4  28643  1to3vfriswmgr  28653  3cyclfrgr  28661  frgrwopreglem5  28694  2clwwlk2clwwlk  28723  numclwlk1lem1  28742  numclwwlk6  28763  ajval  29232  issh  29579  dmadjss  30258  adjeu  30260  adjval  30261  isst  30584  ishst  30585  xrdifh  31110  nndiffz1  31116  xdivpnfrp  31216  isomnd  31336  isslmd  31464  isprmidl  31622  isprmidlc  31632  ismxidl  31643  isrrext  31959  ismntop  31985  isros  32145  issros  32152  issibf  32309  eulerpartleme  32339  eulerpartlemt0  32345  probun  32395  bnj250  32689  bnj255  32693  bnj345  32702  bnj945  32762  bnj1209  32785  bnj1275  32802  bnj543  32882  bnj571  32895  bnj607  32905  bnj882  32915  bnj983  32940  bnj996  32945  bnj1006  32949  bnj1033  32958  bnj1097  32970  bnj1110  32971  bnj1145  32982  bnj1174  32992  bnj1189  32998  bnj1450  33039  bnj1514  33052  cusgr3cyclex  33107  erdszelem1  33162  cvmsval  33237  cvmliftiota  33272  snmlval  33302  lediv2aALT  33644  frxp2  33800  elwlim  33826  nocvxminlem  33981  scutcut  34004  scutbday  34007  brtxp2  34192  brpprod3a  34197  brcart  34243  brsuccf  34252  broutsideof3  34437  ivthALT  34533  df3nandALT2  34598  andnand1  34599  topdifinffinlem  35527  relowlssretop  35543  rdgeqoa  35550  unccur  35769  fin2solem  35772  poimirlem3  35789  poimirlem4  35790  poimirlem26  35812  poimirlem27  35813  poimirlem32  35818  itg2gt0cn  35841  iblabsnclem  35849  areacirc  35879  neificl  35920  ablo4pnp  36047  isrngohom  36132  isidl  36181  ispridl  36201  pridlidl  36202  ismaxidl  36207  maxidlidl  36208  isfldidl2  36236  isdmn3  36241  triantru3  36389  moantr  36501  brxrn2  36512  dfxrn2  36513  ecxrn  36524  inxpxrn  36528  rnxrn  36531  islshp  37000  isopos  37201  cvrfval  37289  cvrval  37290  isatl  37320  isat3  37328  islpln5  37556  4atlem11  37630  dalem20  37714  lhpexle3  38033  lhpex2leN  38034  isltrn2N  38141  diclspsn  39215  lcfls1lem  39555  lcfls1N  39556  uzindd  39992  flt4lem5e  40500  3cubes  40519  fz1eqin  40598  isdomn3  41036  fzunt  41069  fzuntd  41070  fzunt1d  41071  fzuntgd  41072  rp-isfinite6  41132  snhesn  41401  ismnuprim  41919  ismnushort  41926  iotasbc2  42045  eelT00  42332  eelTTT  42333  eelT11  42334  eelT12  42336  eelTT1  42337  eelT01  42338  eel0T1  42339  uun132  42412  uun132p1  42413  un2122  42417  uunTT1  42420  uunTT1p1  42421  uunTT1p2  42422  uunT11  42423  uunT11p1  42424  uunT11p2  42425  uunT12  42426  uunT12p1  42427  uunT12p2  42428  uunT12p3  42429  uunT12p4  42430  uunT12p5  42431  uun111  42432  uun2221  42440  uun2221p1  42441  uun2221p2  42442  stoweidlem17  43565  stoweidlem34  43582  stoweidlem60  43608  ndmaovass  44709  ndmaovdistr  44710  4an21  44773  2elfz3nn0  44819  prproropf1o  44970  fpprel  45191  upwlksfval  45308  isupwlkg  45310  upwlkbprop  45311  isrng  45445  2zrngnmrid  45519  lindslinindsimp2lem5  45814  i0oii  46224  io1ii  46225  sepnsepolem1  46226  iscnrm3lem3  46240  isthincd2  46330  functhinc  46337  elpg  46430  alimp-no-surprise  46496