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  4anpull2  1362  3biant1d  1480  an33rean  1485  cad1  1617  3exdistr  1960  ceqsex2  3504  ceqsex2v  3505  ceqsex3v  3506  ceqsex4v  3507  ceqsex6v  3508  ceqsex8v  3509  2reu5lem1  3729  2reu5lem2  3730  2reu5lem3  3731  eldifpr  4625  rexdifpr  4626  trel3  5227  2rbropap  5529  ordelord  6357  dflim2  6393  dff1o4  6811  foco2  7084  brfvopab  7449  eloprabga  7501  ndmovass  7580  ndmovdistr  7581  dflim3  7826  dflim4  7827  frxp2  8126  mpoxopovel  8202  dfsmo2  8319  dfrecs3  8344  oeeui  8569  naddasslem2  8662  ecopovtrn  8796  elixp2  8877  elixp  8880  mptelixpg  8911  dif1en  9130  dif1enOLD  9132  ssfi  9143  sbthfilem  9168  eqinf  9443  zorn2lem7  10462  grothprim  10794  grothtsk  10795  divmulasscom  11868  muldivdir  11882  divmuldiv  11889  sup3  12147  dfnn3  12207  prime  12622  eluz2  12806  raluz2  12863  elixx1  13322  elixx3g  13326  elioo2  13354  elioo5  13371  elicc4  13381  iccneg  13440  icoshft  13441  difreicc  13452  elfz1  13480  elfz  13481  elfz2  13482  elfzm11  13563  elfz2nn0  13586  elfzo2  13630  elfzo3  13644  lbfzo0  13667  fzo1lb  13681  1elfzo1  13682  fzind2  13753  zmodid2  13868  hashgt23el  14396  swrdnd2  14627  swrdnd0  14629  swrdccatin1  14697  swrdccat  14707  repswswrd  14756  swrdco  14810  2swrd2eqwrdeq  14926  rediv  15104  imdiv  15111  cosmul  16148  bitsval  16401  bitsmod  16413  bitscmp  16415  smueqlem  16467  dfgcd2  16523  lcmneg  16580  lcmftp  16613  coprmgcdb  16626  divgcdcoprmex  16643  cncongr1  16644  cncongr2  16645  difsqpwdvds  16865  oddprmdvds  16881  elgz  16909  xpsfrnel  17532  xpsfrnel2  17534  ismre  17558  mreexexlem4d  17615  iscatd2  17649  isssc  17789  eldmcoa  18034  isdrs  18269  isipodrs  18503  mgmsscl  18579  ismhm  18719  mhmpropd  18726  issubm  18737  issubmndb  18739  submacs  18761  issubg  19065  eqglact  19118  eqgid  19119  ecqusaddd  19131  ecqusaddcl  19132  pgrpsubgsymgbi  19345  isslw  19545  efgsdm  19667  mulgmhm  19764  mulgghm  19765  dmdprd  19937  dprdw  19949  subgdmdprd  19973  dmdprdpr  19988  isrng  20070  issrg  20104  srglmhm  20137  srgrmhm  20138  isring  20153  ringlghm  20228  dfrhm2  20390  issubrng  20463  issubrg3  20516  isdomn3  20631  issdrg  20704  sdrgacs  20717  islmod  20777  lsspropd  20931  islmhm  20941  islbs  20990  lbspropd  21013  qusmulrng  21199  rngqiprngghmlem3  21206  rngqiprnglinlem3  21210  rngqiprnglin  21219  cnfldfunALT  21286  cnfldfunALTOLD  21299  isphl  21544  elocv  21584  isobs  21636  mat1dimscm  22369  scmatghm  22427  scmatmhm  22428  ma1repvcl  22464  smadiadetr  22569  mat2pmatghm  22624  mat2pmatmul  22625  decpmatmulsumfsupp  22667  pm2mpghm  22710  pm2mpmhmlem1  22712  neindisj  23011  lmbrf  23154  hauscmplem  23300  llyi  23368  subislly  23375  islocfin  23411  uptx  23519  txcn  23520  qtopeu  23610  elmptrab  23721  isfbas  23723  trfil2  23781  flimcls  23879  cnextcn  23961  xmetec  24329  ngppropd  24532  ngpocelbl  24599  bl2ioo  24687  xrtgioo  24702  om1elbas  24939  elpi1  24952  isclm  24971  isclmp  25004  isncvsngp  25056  iscph  25077  tcphcph  25144  lmmbr2  25166  lmmbrf  25169  iscau2  25184  caussi  25204  lmclim  25210  bcthlem1  25231  srabn  25267  ishl2  25277  evthicc2  25368  ovolfioo  25375  ovolficc  25376  iblcnlem1  25696  iblrelem  25699  iblre  25702  iblcn  25707  isuc1p  26053  ismon1p  26055  ellogrn  26475  logreclem  26679  atandm  26793  atandm2  26794  atandm3  26795  atans2  26848  dmarea  26874  dchrelbas4  27161  lgsmodeq  27260  lgsmulsqcoprm  27261  nocvxminlem  27696  scutcut  27720  scutbday  27723  addscut2  27893  mulscut2  28043  ax5seg  28872  eengtrkg  28920  uspgredg2v  29158  nb3grpr2  29317  isrusgr0  29501  rusgrprop0  29502  ewlkprop  29538  wksfval  29544  wlkeq  29569  wlkson  29591  wlkonprop  29593  upgr2wlk  29603  upgrtrls  29636  upgristrl  29637  wksonproplem  29639  wksonproplemOLD  29640  pthsfval  29656  ispth  29658  dfpth2  29666  isspthonpth  29686  uhgrwkspth  29692  usgr2wlkspth  29696  crctcshwlkn0lem4  29750  wspthnp  29787  wwlknon  29794  wwlksnextwrd  29834  wwlksnextinj  29836  wspthsnwspthsnon  29853  umgr2adedgwlk  29882  umgr2adedgwlkon  29883  umgr2adedgwlkonALT  29884  umgr2adedgspth  29885  s3wwlks2on  29893  wpthswwlks2on  29898  usgr2wspthons3  29901  usgr2wspthon  29902  elwwlks2  29903  elwspths2spth  29904  rusgrnumwwlkl1  29905  rusgrnumwwlkslem  29906  isclwwlk  29920  clwwlkbp  29921  clwlkclwwlklem3  29937  isclwwlknx  29972  clwwlknp  29973  clwwlkn1  29977  clwwlkn2  29980  clwwlkwwlksb  29990  clwwlknonel  30031  0pth  30061  frcond4  30206  1to3vfriswmgr  30216  3cyclfrgr  30224  frgrwopreglem5  30257  2clwwlk2clwwlk  30286  numclwlk1lem1  30305  numclwwlk6  30326  ajval  30797  issh  31144  dmadjss  31823  adjeu  31825  adjval  31826  isst  32149  ishst  32150  xrdifh  32710  nndiffz1  32716  xdivpnfrp  32860  isomnd  33022  isslmd  33162  isprmidl  33416  isprmidlc  33425  ismxidl  33440  ressply1mon1p  33544  isrrext  33997  ismntop  34023  isros  34165  issros  34172  issibf  34331  eulerpartleme  34361  eulerpartlemt0  34367  probun  34417  bnj250  34698  bnj255  34702  bnj345  34711  bnj945  34770  bnj1209  34793  bnj1275  34810  bnj543  34890  bnj571  34903  bnj607  34913  bnj882  34923  bnj983  34948  bnj996  34953  bnj1006  34957  bnj1033  34966  bnj1097  34978  bnj1110  34979  bnj1145  34990  bnj1174  35000  bnj1189  35006  bnj1450  35047  bnj1514  35060  wevgblacfn  35103  cusgr3cyclex  35130  erdszelem1  35185  cvmsval  35260  cvmliftiota  35295  snmlval  35325  lediv2aALT  35671  elwlim  35818  brtxp2  35876  brpprod3a  35881  brcart  35927  brsuccf  35936  broutsideof3  36121  ivthALT  36330  df3nandALT2  36395  andnand1  36396  topdifinffinlem  37342  relowlssretop  37358  rdgeqoa  37365  unccur  37604  fin2solem  37607  poimirlem3  37624  poimirlem4  37625  poimirlem26  37647  poimirlem27  37648  poimirlem32  37653  itg2gt0cn  37676  iblabsnclem  37684  areacirc  37714  neificl  37754  ablo4pnp  37881  isrngohom  37966  isidl  38015  ispridl  38035  pridlidl  38036  ismaxidl  38041  maxidlidl  38042  isfldidl2  38070  isdmn3  38075  triantru3  38225  moantr  38353  brxrn2  38364  dfxrn2  38365  ecxrn  38380  disjressuc2  38381  inxpxrn  38388  rnxrn  38391  dmqsblocks  38852  islshp  38979  isopos  39180  cvrfval  39268  cvrval  39269  isatl  39299  isat3  39307  islpln5  39536  4atlem11  39610  dalem20  39694  lhpexle3  40013  lhpex2leN  40014  isltrn2N  40121  diclspsn  41195  lcfls1lem  41535  lcfls1N  41536  uzindd  41972  isprimroot  42088  flt4lem5e  42651  3cubes  42685  fz1eqin  42764  dflim6  43260  dflim7  43269  nnoeomeqom  43308  cantnfub2  43318  fzunt  43451  fzuntd  43452  fzunt1d  43453  fzuntgd  43454  rp-isfinite6  43514  snhesn  43782  ismnuprim  44290  ismnushort  44297  iotasbc2  44416  eelT00  44701  eelTTT  44702  eelT11  44703  eelT12  44705  eelTT1  44706  eelT01  44707  eel0T1  44708  uun132  44781  uun132p1  44782  un2122  44786  uunTT1  44789  uunTT1p1  44790  uunTT1p2  44791  uunT11  44792  uunT11p1  44793  uunT11p2  44794  uunT12  44795  uunT12p1  44796  uunT12p2  44797  uunT12p3  44798  uunT12p4  44799  uunT12p5  44800  uun111  44801  uun2221  44809  uun2221p1  44810  uun2221p2  44811  stoweidlem17  46022  stoweidlem34  46039  stoweidlem60  46065  ndmaovass  47211  ndmaovdistr  47212  4an21  47275  2elfz3nn0  47321  difltmodne  47347  prproropf1o  47512  fpprel  47733  clnbgredg  47844  dfvopnbgr2  47857  dfclnbgr6  47860  dfnbgr6  47861  dfsclnbgr6  47862  uhgrimprop  47896  isuspgrimlem  47899  clnbgrgrim  47938  isgrtri  47946  isubgr3stgrlem4  47972  isubgr3stgrlem7  47975  upwlksfval  48127  isupwlkg  48129  upwlkbprop  48130  2zrngnmrid  48248  lindslinindsimp2lem5  48455  i0oii  48912  io1ii  48913  sepnsepolem1  48914  isthincd2  49430  functhinc  49441  elpg  49707  alimp-no-surprise  49774