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  3biant1d  1478  an33rean  1483  cad1  1614  3exdistr  1960  ceqsex2  3547  ceqsex2v  3548  ceqsex3v  3549  ceqsex4v  3550  ceqsex6v  3551  ceqsex8v  3552  2reu5lem1  3777  2reu5lem2  3778  2reu5lem3  3779  eldifpr  4680  rexdifpr  4681  trel3  5293  2rbropap  5585  ordelord  6417  dflim2  6452  dff1o4  6870  foco2  7143  brfvopab  7507  eloprabga  7558  ndmovass  7638  ndmovdistr  7639  dflim3  7884  dflim4  7885  frxp2  8185  mpoxopovel  8261  dfsmo2  8403  dfrecs3  8428  dfrecs3OLD  8429  oeeui  8658  naddasslem2  8751  ecopovtrn  8878  elixp2  8959  elixp  8962  mptelixpg  8993  dif1en  9226  dif1enOLD  9228  ssfi  9240  sbthfilem  9264  eqinf  9553  zorn2lem7  10571  grothprim  10903  grothtsk  10904  divmulasscom  11973  muldivdir  11987  divmuldiv  11994  sup3  12252  dfnn3  12307  prime  12724  eluz2  12909  raluz2  12962  elixx1  13416  elixx3g  13420  elioo2  13448  elioo5  13464  elicc4  13474  iccneg  13532  icoshft  13533  difreicc  13544  elfz1  13572  elfz  13573  elfz2  13574  elfzm11  13655  elfz2nn0  13675  elfzo2  13719  elfzo3  13733  lbfzo0  13756  fzind2  13835  zmodid2  13950  hashgt23el  14473  swrdnd2  14703  swrdnd0  14705  swrdccatin1  14773  swrdccat  14783  repswswrd  14832  swrdco  14886  2swrd2eqwrdeq  15002  rediv  15180  imdiv  15187  cosmul  16221  bitsval  16470  bitsmod  16482  bitscmp  16484  smueqlem  16536  dfgcd2  16593  lcmneg  16650  lcmftp  16683  coprmgcdb  16696  divgcdcoprmex  16713  cncongr1  16714  cncongr2  16715  difsqpwdvds  16934  oddprmdvds  16950  elgz  16978  xpsfrnel  17622  xpsfrnel2  17624  ismre  17648  mreexexlem4d  17705  iscatd2  17739  isssc  17881  eldmcoa  18132  isdrs  18371  isipodrs  18607  mgmsscl  18683  ismhm  18820  mhmpropd  18827  issubm  18838  issubmndb  18840  submacs  18862  issubg  19166  eqglact  19219  eqgid  19220  ecqusaddd  19232  ecqusaddcl  19233  pgrpsubgsymgbi  19450  isslw  19650  efgsdm  19772  mulgmhm  19869  mulgghm  19870  dmdprd  20042  dprdw  20054  subgdmdprd  20078  dmdprdpr  20093  isrng  20181  issrg  20215  srglmhm  20248  srgrmhm  20249  isring  20264  ringlghm  20335  dfrhm2  20500  issubrng  20573  issubrg3  20628  isdomn3  20737  issdrg  20811  sdrgacs  20824  islmod  20884  lsspropd  21039  islmhm  21049  islbs  21098  lbspropd  21121  qusmulrng  21315  rngqiprngghmlem3  21322  rngqiprnglinlem3  21326  rngqiprnglin  21335  cnfldfunALT  21402  cnfldfunALTOLD  21415  isphl  21669  elocv  21709  isobs  21763  mat1dimscm  22502  scmatghm  22560  scmatmhm  22561  ma1repvcl  22597  smadiadetr  22702  mat2pmatghm  22757  mat2pmatmul  22758  decpmatmulsumfsupp  22800  pm2mpghm  22843  pm2mpmhmlem1  22845  neindisj  23146  lmbrf  23289  hauscmplem  23435  llyi  23503  subislly  23510  islocfin  23546  uptx  23654  txcn  23655  qtopeu  23745  elmptrab  23856  isfbas  23858  trfil2  23916  flimcls  24014  cnextcn  24096  xmetec  24465  ngppropd  24671  ngpocelbl  24746  bl2ioo  24833  xrtgioo  24847  om1elbas  25084  elpi1  25097  isclm  25116  isclmp  25149  isncvsngp  25202  iscph  25223  tcphcph  25290  lmmbr2  25312  lmmbrf  25315  iscau2  25330  caussi  25350  lmclim  25356  bcthlem1  25377  srabn  25413  ishl2  25423  evthicc2  25514  ovolfioo  25521  ovolficc  25522  iblcnlem1  25843  iblrelem  25846  iblre  25849  iblcn  25854  isuc1p  26200  ismon1p  26202  ellogrn  26619  logreclem  26823  atandm  26937  atandm2  26938  atandm3  26939  atans2  26992  dmarea  27018  dchrelbas4  27305  lgsmodeq  27404  lgsmulsqcoprm  27405  nocvxminlem  27840  scutcut  27864  scutbday  27867  addscut2  28030  mulscut2  28177  ax5seg  28971  eengtrkg  29019  uspgredg2v  29259  nb3grpr2  29418  isrusgr0  29602  rusgrprop0  29603  ewlkprop  29639  wksfval  29645  wlkeq  29670  wlkson  29692  wlkonprop  29694  upgr2wlk  29704  upgrtrls  29737  upgristrl  29738  wksonproplem  29740  wksonproplemOLD  29741  pthsfval  29757  ispth  29759  isspthonpth  29785  uhgrwkspth  29791  usgr2wlkspth  29795  crctcshwlkn0lem4  29846  wspthnp  29883  wwlknon  29890  wwlksnextwrd  29930  wwlksnextinj  29932  wspthsnwspthsnon  29949  umgr2adedgwlk  29978  umgr2adedgwlkon  29979  umgr2adedgwlkonALT  29980  umgr2adedgspth  29981  s3wwlks2on  29989  wpthswwlks2on  29994  usgr2wspthons3  29997  usgr2wspthon  29998  elwwlks2  29999  elwspths2spth  30000  rusgrnumwwlkl1  30001  rusgrnumwwlkslem  30002  isclwwlk  30016  clwwlkbp  30017  clwlkclwwlklem3  30033  isclwwlknx  30068  clwwlknp  30069  clwwlkn1  30073  clwwlkn2  30076  clwwlkwwlksb  30086  clwwlknonel  30127  0pth  30157  frcond4  30302  1to3vfriswmgr  30312  3cyclfrgr  30320  frgrwopreglem5  30353  2clwwlk2clwwlk  30382  numclwlk1lem1  30401  numclwwlk6  30422  ajval  30893  issh  31240  dmadjss  31919  adjeu  31921  adjval  31922  isst  32245  ishst  32246  xrdifh  32785  nndiffz1  32791  xdivpnfrp  32897  isomnd  33051  isslmd  33181  isprmidl  33431  isprmidlc  33440  ismxidl  33455  ressply1mon1p  33558  isrrext  33946  ismntop  33972  isros  34132  issros  34139  issibf  34298  eulerpartleme  34328  eulerpartlemt0  34334  probun  34384  bnj250  34677  bnj255  34681  bnj345  34690  bnj945  34749  bnj1209  34772  bnj1275  34789  bnj543  34869  bnj571  34882  bnj607  34892  bnj882  34902  bnj983  34927  bnj996  34932  bnj1006  34936  bnj1033  34945  bnj1097  34957  bnj1110  34958  bnj1145  34969  bnj1174  34979  bnj1189  34985  bnj1450  35026  bnj1514  35039  wevgblacfn  35076  cusgr3cyclex  35104  erdszelem1  35159  cvmsval  35234  cvmliftiota  35269  snmlval  35299  lediv2aALT  35645  elwlim  35787  brtxp2  35845  brpprod3a  35850  brcart  35896  brsuccf  35905  broutsideof3  36090  ivthALT  36301  df3nandALT2  36366  andnand1  36367  topdifinffinlem  37313  relowlssretop  37329  rdgeqoa  37336  unccur  37563  fin2solem  37566  poimirlem3  37583  poimirlem4  37584  poimirlem26  37606  poimirlem27  37607  poimirlem32  37612  itg2gt0cn  37635  iblabsnclem  37643  areacirc  37673  neificl  37713  ablo4pnp  37840  isrngohom  37925  isidl  37974  ispridl  37994  pridlidl  37995  ismaxidl  38000  maxidlidl  38001  isfldidl2  38029  isdmn3  38034  triantru3  38184  moantr  38320  brxrn2  38331  dfxrn2  38332  ecxrn  38343  disjressuc2  38344  inxpxrn  38351  rnxrn  38354  islshp  38935  isopos  39136  cvrfval  39224  cvrval  39225  isatl  39255  isat3  39263  islpln5  39492  4atlem11  39566  dalem20  39650  lhpexle3  39969  lhpex2leN  39970  isltrn2N  40077  diclspsn  41151  lcfls1lem  41491  lcfls1N  41492  uzindd  41933  isprimroot  42050  flt4lem5e  42611  3cubes  42646  fz1eqin  42725  dflim6  43226  dflim7  43235  nnoeomeqom  43274  cantnfub2  43284  fzunt  43417  fzuntd  43418  fzunt1d  43419  fzuntgd  43420  rp-isfinite6  43480  snhesn  43748  ismnuprim  44263  ismnushort  44270  iotasbc2  44389  eelT00  44676  eelTTT  44677  eelT11  44678  eelT12  44680  eelTT1  44681  eelT01  44682  eel0T1  44683  uun132  44756  uun132p1  44757  un2122  44761  uunTT1  44764  uunTT1p1  44765  uunTT1p2  44766  uunT11  44767  uunT11p1  44768  uunT11p2  44769  uunT12  44770  uunT12p1  44771  uunT12p2  44772  uunT12p3  44773  uunT12p4  44774  uunT12p5  44775  uun111  44776  uun2221  44784  uun2221p1  44785  uun2221p2  44786  stoweidlem17  45938  stoweidlem34  45955  stoweidlem60  45981  ndmaovass  47121  ndmaovdistr  47122  4an21  47185  2elfz3nn0  47231  prproropf1o  47381  fpprel  47602  clnbgredg  47712  dfvopnbgr2  47725  dfclnbgr6  47728  dfnbgr6  47729  dfsclnbgr6  47730  uspgrimprop  47757  isuspgrimlem  47758  clnbgrgrim  47786  isgrtri  47794  upwlksfval  47858  isupwlkg  47860  upwlkbprop  47861  2zrngnmrid  47979  lindslinindsimp2lem5  48191  i0oii  48599  io1ii  48600  sepnsepolem1  48601  iscnrm3lem3  48615  isthincd2  48705  functhinc  48712  elpg  48806  alimp-no-surprise  48875