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  3492  ceqsex2v  3493  ceqsex3v  3494  ceqsex4v  3495  ceqsex6v  3496  ceqsex8v  3497  2reu5lem1  3712  2reu5lem2  3713  2reu5lem3  3714  eldifpr  4614  rexdifpr  4615  trel3  5213  2rbropap  5511  ordelord  6338  dflim2  6374  dff1o4  6781  foco2  7054  brfvopab  7415  eloprabga  7467  ndmovass  7546  ndmovdistr  7547  dflim3  7789  dflim4  7790  frxp2  8086  mpoxopovel  8162  dfsmo2  8279  dfrecs3  8304  oeeui  8530  naddasslem2  8623  ecopovtrn  8759  elixp2  8841  elixp  8844  mptelixpg  8875  dif1en  9088  ssfi  9099  sbthfilem  9124  eqinf  9390  zorn2lem7  10414  grothprim  10747  grothtsk  10748  divmulasscom  11822  muldivdir  11836  divmuldiv  11843  sup3  12101  dfnn3  12161  prime  12575  eluz2  12759  raluz2  12812  elixx1  13272  elixx3g  13276  elioo2  13304  elioo5  13321  elicc4  13331  iccneg  13390  icoshft  13391  difreicc  13402  elfz1  13430  elfz  13431  elfz2  13432  elfzm11  13513  elfz2nn0  13536  elfzo2  13580  elfzo3  13594  lbfzo0  13617  fzo1lb  13631  1elfzo1  13632  fzind2  13706  zmodid2  13821  hashgt23el  14349  swrdnd2  14581  swrdnd0  14583  swrdccatin1  14650  swrdccat  14660  repswswrd  14709  swrdco  14762  2swrd2eqwrdeq  14878  rediv  15056  imdiv  15063  cosmul  16100  bitsval  16353  bitsmod  16365  bitscmp  16367  smueqlem  16419  dfgcd2  16475  lcmneg  16532  lcmftp  16565  coprmgcdb  16578  divgcdcoprmex  16595  cncongr1  16596  cncongr2  16597  difsqpwdvds  16817  oddprmdvds  16833  elgz  16861  xpsfrnel  17485  xpsfrnel2  17487  ismre  17511  mreexexlem4d  17572  iscatd2  17606  isssc  17746  eldmcoa  17991  isdrs  18226  isipodrs  18462  mgmsscl  18572  ismhm  18712  mhmpropd  18719  issubm  18730  issubmndb  18732  submacs  18754  issubg  19058  eqglact  19110  eqgid  19111  ecqusaddd  19123  ecqusaddcl  19124  pgrpsubgsymgbi  19339  isslw  19539  efgsdm  19661  mulgmhm  19758  mulgghm  19759  dmdprd  19931  dprdw  19943  subgdmdprd  19967  dmdprdpr  19982  isomnd  20054  isrng  20091  issrg  20125  srglmhm  20158  srgrmhm  20159  isring  20174  ringlghm  20249  dfrhm2  20412  issubrng  20482  issubrg3  20535  isdomn3  20650  issdrg  20723  sdrgacs  20736  islmod  20817  lsspropd  20971  islmhm  20981  islbs  21030  lbspropd  21053  qusmulrng  21239  rngqiprngghmlem3  21246  rngqiprnglinlem3  21250  rngqiprnglin  21259  cnfldfunALT  21326  cnfldfunALTOLD  21339  isphl  21585  elocv  21625  isobs  21677  mat1dimscm  22421  scmatghm  22479  scmatmhm  22480  ma1repvcl  22516  smadiadetr  22621  mat2pmatghm  22676  mat2pmatmul  22677  decpmatmulsumfsupp  22719  pm2mpghm  22762  pm2mpmhmlem1  22764  neindisj  23063  lmbrf  23206  hauscmplem  23352  llyi  23420  subislly  23427  islocfin  23463  uptx  23571  txcn  23572  qtopeu  23662  elmptrab  23773  isfbas  23775  trfil2  23833  flimcls  23931  cnextcn  24013  xmetec  24380  ngppropd  24583  ngpocelbl  24650  bl2ioo  24738  xrtgioo  24753  om1elbas  24990  elpi1  25003  isclm  25022  isclmp  25055  isncvsngp  25107  iscph  25128  tcphcph  25195  lmmbr2  25217  lmmbrf  25220  iscau2  25235  caussi  25255  lmclim  25261  bcthlem1  25282  srabn  25318  ishl2  25328  evthicc2  25419  ovolfioo  25426  ovolficc  25427  iblcnlem1  25747  iblrelem  25750  iblre  25753  iblcn  25758  isuc1p  26104  ismon1p  26106  ellogrn  26526  logreclem  26730  atandm  26844  atandm2  26845  atandm3  26846  atans2  26899  dmarea  26925  dchrelbas4  27212  lgsmodeq  27311  lgsmulsqcoprm  27312  nocvxminlem  27752  scutcut  27777  scutbday  27780  addscut2  27959  mulscut2  28113  ax5seg  28992  eengtrkg  29040  uspgredg2v  29278  nb3grpr2  29437  isrusgr0  29621  rusgrprop0  29622  ewlkprop  29658  wksfval  29664  wlkeq  29688  wlkson  29709  wlkonprop  29711  upgr2wlk  29721  upgrtrls  29754  upgristrl  29755  wksonproplem  29757  pthsfval  29773  ispth  29775  dfpth2  29783  isspthonpth  29803  uhgrwkspth  29809  usgr2wlkspth  29813  crctcshwlkn0lem4  29867  wspthnp  29904  wwlknon  29911  wwlksnextwrd  29951  wwlksnextinj  29953  wspthsnwspthsnon  29970  umgr2adedgwlk  29999  umgr2adedgwlkon  30000  umgr2adedgwlkonALT  30001  umgr2adedgspth  30002  s3wwlks2on  30010  sps3wwlks2on  30011  wpthswwlks2on  30018  usgr2wspthons3  30021  usgr2wspthon  30022  elwwlks2  30023  elwspths2spth  30024  rusgrnumwwlkl1  30025  rusgrnumwwlkslem  30026  isclwwlk  30040  clwwlkbp  30041  clwlkclwwlklem3  30057  isclwwlknx  30092  clwwlknp  30093  clwwlkn1  30097  clwwlkn2  30100  clwwlkwwlksb  30110  clwwlknonel  30151  0pth  30181  frcond4  30326  1to3vfriswmgr  30336  3cyclfrgr  30344  frgrwopreglem5  30377  2clwwlk2clwwlk  30406  numclwlk1lem1  30425  numclwwlk6  30446  ajval  30917  issh  31264  dmadjss  31943  adjeu  31945  adjval  31946  isst  32269  ishst  32270  xrdifh  32839  nndiffz1  32845  xdivpnfrp  32993  isslmd  33263  isprmidl  33498  isprmidlc  33507  ismxidl  33522  ressply1mon1p  33628  isrrext  34136  ismntop  34162  isros  34304  issros  34311  issibf  34469  eulerpartleme  34499  eulerpartlemt0  34505  probun  34555  bnj250  34836  bnj255  34840  bnj345  34849  bnj945  34908  bnj1209  34931  bnj1275  34948  bnj543  35028  bnj571  35041  bnj607  35051  bnj882  35061  bnj983  35086  bnj996  35091  bnj1006  35095  bnj1033  35104  bnj1097  35116  bnj1110  35117  bnj1145  35128  bnj1174  35138  bnj1189  35144  bnj1450  35185  bnj1514  35198  wevgblacfn  35282  cusgr3cyclex  35309  erdszelem1  35364  cvmsval  35439  cvmliftiota  35474  snmlval  35504  lediv2aALT  35850  elwlim  35994  brtxp2  36052  brpprod3a  36057  brcart  36103  lemsuccf  36112  broutsideof3  36299  ivthALT  36508  df3nandALT2  36573  andnand1  36574  topdifinffinlem  37521  relowlssretop  37537  rdgeqoa  37544  unccur  37773  fin2solem  37776  poimirlem3  37793  poimirlem4  37794  poimirlem26  37816  poimirlem27  37817  poimirlem32  37822  itg2gt0cn  37845  iblabsnclem  37853  areacirc  37883  neificl  37923  ablo4pnp  38050  isrngohom  38135  isidl  38184  ispridl  38204  pridlidl  38205  ismaxidl  38210  maxidlidl  38211  isfldidl2  38239  isdmn3  38244  triantru3  38406  moantr  38542  brxrn2  38554  dfxrn2  38555  ecxrn  38576  disjressuc2  38581  inxpxrn  38588  rnxrn  38591  dfsuccl4  38644  dmqsblocks  39137  islshp  39274  isopos  39475  cvrfval  39563  cvrval  39564  isatl  39594  isat3  39602  islpln5  39830  4atlem11  39904  dalem20  39988  lhpexle3  40307  lhpex2leN  40308  isltrn2N  40415  diclspsn  41489  lcfls1lem  41829  lcfls1N  41830  uzindd  42266  isprimroot  42382  flt4lem5e  42936  3cubes  42969  fz1eqin  43048  dflim6  43543  dflim7  43552  nnoeomeqom  43591  cantnfub2  43601  fzunt  43733  fzuntd  43734  fzunt1d  43735  fzuntgd  43736  rp-isfinite6  43796  snhesn  44064  ismnuprim  44572  ismnushort  44579  iotasbc2  44698  eelT00  44982  eelTTT  44983  eelT11  44984  eelT12  44986  eelTT1  44987  eelT01  44988  eel0T1  44989  uun132  45062  uun132p1  45063  un2122  45067  uunTT1  45070  uunTT1p1  45071  uunTT1p2  45072  uunT11  45073  uunT11p1  45074  uunT11p2  45075  uunT12  45076  uunT12p1  45077  uunT12p2  45078  uunT12p3  45079  uunT12p4  45080  uunT12p5  45081  uun111  45082  uun2221  45090  uun2221p1  45091  uun2221p2  45092  stoweidlem17  46298  stoweidlem34  46315  stoweidlem60  46341  ndmaovass  47489  ndmaovdistr  47490  4an21  47553  2elfz3nn0  47599  difltmodne  47625  prproropf1o  47790  fpprel  48011  clnbgredg  48123  dfvopnbgr2  48136  dfclnbgr6  48139  dfnbgr6  48140  dfsclnbgr6  48141  uhgrimprop  48175  isuspgrimlem  48178  clnbgrgrim  48217  isgrtri  48226  isubgr3stgrlem4  48252  isubgr3stgrlem7  48255  upwlksfval  48418  isupwlkg  48420  upwlkbprop  48421  2zrngnmrid  48539  lindslinindsimp2lem5  48745  i0oii  49202  io1ii  49203  sepnsepolem1  49204  isthincd2  49719  functhinc  49730  elpg  49996  alimp-no-surprise  50063