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

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3anan12  1095  3ancoma  1097  anandi3  1101  3biant1d  1477  an33rean  1482  cad1  1613  3exdistr  1957  ceqsex2  3534  ceqsex2v  3535  ceqsex3v  3536  ceqsex4v  3537  ceqsex6v  3538  ceqsex8v  3539  2reu5lem1  3763  2reu5lem2  3764  2reu5lem3  3765  eldifpr  4662  rexdifpr  4663  trel3  5274  2rbropap  5575  ordelord  6407  dflim2  6442  dff1o4  6856  foco2  7128  brfvopab  7489  eloprabga  7540  ndmovass  7620  ndmovdistr  7621  dflim3  7867  dflim4  7868  frxp2  8167  mpoxopovel  8243  dfsmo2  8385  dfrecs3  8410  dfrecs3OLD  8411  oeeui  8638  naddasslem2  8731  ecopovtrn  8858  elixp2  8939  elixp  8942  mptelixpg  8973  dif1en  9198  dif1enOLD  9200  ssfi  9211  sbthfilem  9235  eqinf  9521  zorn2lem7  10539  grothprim  10871  grothtsk  10872  divmulasscom  11943  muldivdir  11957  divmuldiv  11964  sup3  12222  dfnn3  12277  prime  12696  eluz2  12881  raluz2  12936  elixx1  13392  elixx3g  13396  elioo2  13424  elioo5  13440  elicc4  13450  iccneg  13508  icoshft  13509  difreicc  13520  elfz1  13548  elfz  13549  elfz2  13550  elfzm11  13631  elfz2nn0  13654  elfzo2  13698  elfzo3  13712  lbfzo0  13735  fzo1lb  13749  fzind2  13820  zmodid2  13935  hashgt23el  14459  swrdnd2  14689  swrdnd0  14691  swrdccatin1  14759  swrdccat  14769  repswswrd  14818  swrdco  14872  2swrd2eqwrdeq  14988  rediv  15166  imdiv  15173  cosmul  16205  bitsval  16457  bitsmod  16469  bitscmp  16471  smueqlem  16523  dfgcd2  16579  lcmneg  16636  lcmftp  16669  coprmgcdb  16682  divgcdcoprmex  16699  cncongr1  16700  cncongr2  16701  difsqpwdvds  16920  oddprmdvds  16936  elgz  16964  xpsfrnel  17608  xpsfrnel2  17610  ismre  17634  mreexexlem4d  17691  iscatd2  17725  isssc  17867  eldmcoa  18118  isdrs  18358  isipodrs  18594  mgmsscl  18670  ismhm  18810  mhmpropd  18817  issubm  18828  issubmndb  18830  submacs  18852  issubg  19156  eqglact  19209  eqgid  19210  ecqusaddd  19222  ecqusaddcl  19223  pgrpsubgsymgbi  19440  isslw  19640  efgsdm  19762  mulgmhm  19859  mulgghm  19860  dmdprd  20032  dprdw  20044  subgdmdprd  20068  dmdprdpr  20083  isrng  20171  issrg  20205  srglmhm  20238  srgrmhm  20239  isring  20254  ringlghm  20325  dfrhm2  20490  issubrng  20563  issubrg3  20616  isdomn3  20731  issdrg  20805  sdrgacs  20818  islmod  20878  lsspropd  21033  islmhm  21043  islbs  21092  lbspropd  21115  qusmulrng  21309  rngqiprngghmlem3  21316  rngqiprnglinlem3  21320  rngqiprnglin  21329  cnfldfunALT  21396  cnfldfunALTOLD  21409  isphl  21663  elocv  21703  isobs  21757  mat1dimscm  22496  scmatghm  22554  scmatmhm  22555  ma1repvcl  22591  smadiadetr  22696  mat2pmatghm  22751  mat2pmatmul  22752  decpmatmulsumfsupp  22794  pm2mpghm  22837  pm2mpmhmlem1  22839  neindisj  23140  lmbrf  23283  hauscmplem  23429  llyi  23497  subislly  23504  islocfin  23540  uptx  23648  txcn  23649  qtopeu  23739  elmptrab  23850  isfbas  23852  trfil2  23910  flimcls  24008  cnextcn  24090  xmetec  24459  ngppropd  24665  ngpocelbl  24740  bl2ioo  24827  xrtgioo  24841  om1elbas  25078  elpi1  25091  isclm  25110  isclmp  25143  isncvsngp  25196  iscph  25217  tcphcph  25284  lmmbr2  25306  lmmbrf  25309  iscau2  25324  caussi  25344  lmclim  25350  bcthlem1  25371  srabn  25407  ishl2  25417  evthicc2  25508  ovolfioo  25515  ovolficc  25516  iblcnlem1  25837  iblrelem  25840  iblre  25843  iblcn  25848  isuc1p  26194  ismon1p  26196  ellogrn  26615  logreclem  26819  atandm  26933  atandm2  26934  atandm3  26935  atans2  26988  dmarea  27014  dchrelbas4  27301  lgsmodeq  27400  lgsmulsqcoprm  27401  nocvxminlem  27836  scutcut  27860  scutbday  27863  addscut2  28026  mulscut2  28173  ax5seg  28967  eengtrkg  29015  uspgredg2v  29255  nb3grpr2  29414  isrusgr0  29598  rusgrprop0  29599  ewlkprop  29635  wksfval  29641  wlkeq  29666  wlkson  29688  wlkonprop  29690  upgr2wlk  29700  upgrtrls  29733  upgristrl  29734  wksonproplem  29736  wksonproplemOLD  29737  pthsfval  29753  ispth  29755  isspthonpth  29781  uhgrwkspth  29787  usgr2wlkspth  29791  crctcshwlkn0lem4  29842  wspthnp  29879  wwlknon  29886  wwlksnextwrd  29926  wwlksnextinj  29928  wspthsnwspthsnon  29945  umgr2adedgwlk  29974  umgr2adedgwlkon  29975  umgr2adedgwlkonALT  29976  umgr2adedgspth  29977  s3wwlks2on  29985  wpthswwlks2on  29990  usgr2wspthons3  29993  usgr2wspthon  29994  elwwlks2  29995  elwspths2spth  29996  rusgrnumwwlkl1  29997  rusgrnumwwlkslem  29998  isclwwlk  30012  clwwlkbp  30013  clwlkclwwlklem3  30029  isclwwlknx  30064  clwwlknp  30065  clwwlkn1  30069  clwwlkn2  30072  clwwlkwwlksb  30082  clwwlknonel  30123  0pth  30153  frcond4  30298  1to3vfriswmgr  30308  3cyclfrgr  30316  frgrwopreglem5  30349  2clwwlk2clwwlk  30378  numclwlk1lem1  30397  numclwwlk6  30418  ajval  30889  issh  31236  dmadjss  31915  adjeu  31917  adjval  31918  isst  32241  ishst  32242  xrdifh  32788  nndiffz1  32794  xdivpnfrp  32899  isomnd  33060  isslmd  33190  isprmidl  33445  isprmidlc  33454  ismxidl  33469  ressply1mon1p  33572  isrrext  33962  ismntop  33988  isros  34148  issros  34155  issibf  34314  eulerpartleme  34344  eulerpartlemt0  34350  probun  34400  bnj250  34693  bnj255  34697  bnj345  34706  bnj945  34765  bnj1209  34788  bnj1275  34805  bnj543  34885  bnj571  34898  bnj607  34908  bnj882  34918  bnj983  34943  bnj996  34948  bnj1006  34952  bnj1033  34961  bnj1097  34973  bnj1110  34974  bnj1145  34985  bnj1174  34995  bnj1189  35001  bnj1450  35042  bnj1514  35055  wevgblacfn  35092  cusgr3cyclex  35120  erdszelem1  35175  cvmsval  35250  cvmliftiota  35285  snmlval  35315  lediv2aALT  35661  elwlim  35804  brtxp2  35862  brpprod3a  35867  brcart  35913  brsuccf  35922  broutsideof3  36107  ivthALT  36317  df3nandALT2  36382  andnand1  36383  topdifinffinlem  37329  relowlssretop  37345  rdgeqoa  37352  unccur  37589  fin2solem  37592  poimirlem3  37609  poimirlem4  37610  poimirlem26  37632  poimirlem27  37633  poimirlem32  37638  itg2gt0cn  37661  iblabsnclem  37669  areacirc  37699  neificl  37739  ablo4pnp  37866  isrngohom  37951  isidl  38000  ispridl  38020  pridlidl  38021  ismaxidl  38026  maxidlidl  38027  isfldidl2  38055  isdmn3  38060  triantru3  38210  moantr  38345  brxrn2  38356  dfxrn2  38357  ecxrn  38368  disjressuc2  38369  inxpxrn  38376  rnxrn  38379  islshp  38960  isopos  39161  cvrfval  39249  cvrval  39250  isatl  39280  isat3  39288  islpln5  39517  4atlem11  39591  dalem20  39675  lhpexle3  39994  lhpex2leN  39995  isltrn2N  40102  diclspsn  41176  lcfls1lem  41516  lcfls1N  41517  uzindd  41958  isprimroot  42074  flt4lem5e  42642  3cubes  42677  fz1eqin  42756  dflim6  43253  dflim7  43262  nnoeomeqom  43301  cantnfub2  43311  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  rp-isfinite6  43507  snhesn  43775  ismnuprim  44289  ismnushort  44296  iotasbc2  44415  eelT00  44702  eelTTT  44703  eelT11  44704  eelT12  44706  eelTT1  44707  eelT01  44708  eel0T1  44709  uun132  44782  uun132p1  44783  un2122  44787  uunTT1  44790  uunTT1p1  44791  uunTT1p2  44792  uunT11  44793  uunT11p1  44794  uunT11p2  44795  uunT12  44796  uunT12p1  44797  uunT12p2  44798  uunT12p3  44799  uunT12p4  44800  uunT12p5  44801  uun111  44802  uun2221  44810  uun2221p1  44811  uun2221p2  44812  stoweidlem17  45972  stoweidlem34  45989  stoweidlem60  46015  ndmaovass  47155  ndmaovdistr  47156  4an21  47219  2elfz3nn0  47265  difltmodne  47281  prproropf1o  47431  fpprel  47652  clnbgredg  47763  dfvopnbgr2  47776  dfclnbgr6  47779  dfnbgr6  47780  dfsclnbgr6  47781  uspgrimprop  47810  isuspgrimlem  47811  clnbgrgrim  47839  isgrtri  47847  isubgr3stgrlem4  47871  isubgr3stgrlem7  47874  upwlksfval  47978  isupwlkg  47980  upwlkbprop  47981  2zrngnmrid  48099  lindslinindsimp2lem5  48307  i0oii  48715  io1ii  48716  sepnsepolem1  48717  iscnrm3lem3  48731  isthincd2  48837  functhinc  48844  elpg  48944  alimp-no-surprise  49011