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  3498  ceqsex2v  3499  ceqsex3v  3500  ceqsex4v  3501  ceqsex6v  3502  ceqsex8v  3503  2reu5lem1  3723  2reu5lem2  3724  2reu5lem3  3725  eldifpr  4618  rexdifpr  4619  trel3  5219  2rbropap  5519  ordelord  6342  dflim2  6378  dff1o4  6790  foco2  7063  brfvopab  7426  eloprabga  7478  ndmovass  7557  ndmovdistr  7558  dflim3  7803  dflim4  7804  frxp2  8100  mpoxopovel  8176  dfsmo2  8293  dfrecs3  8318  oeeui  8543  naddasslem2  8636  ecopovtrn  8770  elixp2  8851  elixp  8854  mptelixpg  8885  dif1en  9101  dif1enOLD  9103  ssfi  9114  sbthfilem  9139  eqinf  9412  zorn2lem7  10433  grothprim  10765  grothtsk  10766  divmulasscom  11839  muldivdir  11853  divmuldiv  11860  sup3  12118  dfnn3  12178  prime  12593  eluz2  12777  raluz2  12834  elixx1  13293  elixx3g  13297  elioo2  13325  elioo5  13342  elicc4  13352  iccneg  13411  icoshft  13412  difreicc  13423  elfz1  13451  elfz  13452  elfz2  13453  elfzm11  13534  elfz2nn0  13557  elfzo2  13601  elfzo3  13615  lbfzo0  13638  fzo1lb  13652  1elfzo1  13653  fzind2  13724  zmodid2  13839  hashgt23el  14367  swrdnd2  14598  swrdnd0  14600  swrdccatin1  14667  swrdccat  14677  repswswrd  14726  swrdco  14780  2swrd2eqwrdeq  14896  rediv  15074  imdiv  15081  cosmul  16118  bitsval  16371  bitsmod  16383  bitscmp  16385  smueqlem  16437  dfgcd2  16493  lcmneg  16550  lcmftp  16583  coprmgcdb  16596  divgcdcoprmex  16613  cncongr1  16614  cncongr2  16615  difsqpwdvds  16835  oddprmdvds  16851  elgz  16879  xpsfrnel  17502  xpsfrnel2  17504  ismre  17528  mreexexlem4d  17589  iscatd2  17623  isssc  17763  eldmcoa  18008  isdrs  18243  isipodrs  18479  mgmsscl  18555  ismhm  18695  mhmpropd  18702  issubm  18713  issubmndb  18715  submacs  18737  issubg  19041  eqglact  19094  eqgid  19095  ecqusaddd  19107  ecqusaddcl  19108  pgrpsubgsymgbi  19323  isslw  19523  efgsdm  19645  mulgmhm  19742  mulgghm  19743  dmdprd  19915  dprdw  19927  subgdmdprd  19951  dmdprdpr  19966  isomnd  20038  isrng  20075  issrg  20109  srglmhm  20142  srgrmhm  20143  isring  20158  ringlghm  20233  dfrhm2  20395  issubrng  20468  issubrg3  20521  isdomn3  20636  issdrg  20709  sdrgacs  20722  islmod  20803  lsspropd  20957  islmhm  20967  islbs  21016  lbspropd  21039  qusmulrng  21225  rngqiprngghmlem3  21232  rngqiprnglinlem3  21236  rngqiprnglin  21245  cnfldfunALT  21312  cnfldfunALTOLD  21325  isphl  21571  elocv  21611  isobs  21663  mat1dimscm  22396  scmatghm  22454  scmatmhm  22455  ma1repvcl  22491  smadiadetr  22596  mat2pmatghm  22651  mat2pmatmul  22652  decpmatmulsumfsupp  22694  pm2mpghm  22737  pm2mpmhmlem1  22739  neindisj  23038  lmbrf  23181  hauscmplem  23327  llyi  23395  subislly  23402  islocfin  23438  uptx  23546  txcn  23547  qtopeu  23637  elmptrab  23748  isfbas  23750  trfil2  23808  flimcls  23906  cnextcn  23988  xmetec  24356  ngppropd  24559  ngpocelbl  24626  bl2ioo  24714  xrtgioo  24729  om1elbas  24966  elpi1  24979  isclm  24998  isclmp  25031  isncvsngp  25083  iscph  25104  tcphcph  25171  lmmbr2  25193  lmmbrf  25196  iscau2  25211  caussi  25231  lmclim  25237  bcthlem1  25258  srabn  25294  ishl2  25304  evthicc2  25395  ovolfioo  25402  ovolficc  25403  iblcnlem1  25723  iblrelem  25726  iblre  25729  iblcn  25734  isuc1p  26080  ismon1p  26082  ellogrn  26502  logreclem  26706  atandm  26820  atandm2  26821  atandm3  26822  atans2  26875  dmarea  26901  dchrelbas4  27188  lgsmodeq  27287  lgsmulsqcoprm  27288  nocvxminlem  27724  scutcut  27748  scutbday  27751  addscut2  27927  mulscut2  28077  ax5seg  28919  eengtrkg  28967  uspgredg2v  29205  nb3grpr2  29364  isrusgr0  29548  rusgrprop0  29549  ewlkprop  29585  wksfval  29591  wlkeq  29615  wlkson  29636  wlkonprop  29638  upgr2wlk  29648  upgrtrls  29681  upgristrl  29682  wksonproplem  29684  pthsfval  29700  ispth  29702  dfpth2  29710  isspthonpth  29730  uhgrwkspth  29736  usgr2wlkspth  29740  crctcshwlkn0lem4  29794  wspthnp  29831  wwlknon  29838  wwlksnextwrd  29878  wwlksnextinj  29880  wspthsnwspthsnon  29897  umgr2adedgwlk  29926  umgr2adedgwlkon  29927  umgr2adedgwlkonALT  29928  umgr2adedgspth  29929  s3wwlks2on  29937  wpthswwlks2on  29942  usgr2wspthons3  29945  usgr2wspthon  29946  elwwlks2  29947  elwspths2spth  29948  rusgrnumwwlkl1  29949  rusgrnumwwlkslem  29950  isclwwlk  29964  clwwlkbp  29965  clwlkclwwlklem3  29981  isclwwlknx  30016  clwwlknp  30017  clwwlkn1  30021  clwwlkn2  30024  clwwlkwwlksb  30034  clwwlknonel  30075  0pth  30105  frcond4  30250  1to3vfriswmgr  30260  3cyclfrgr  30268  frgrwopreglem5  30301  2clwwlk2clwwlk  30330  numclwlk1lem1  30349  numclwwlk6  30370  ajval  30841  issh  31188  dmadjss  31867  adjeu  31869  adjval  31870  isst  32193  ishst  32194  xrdifh  32754  nndiffz1  32760  xdivpnfrp  32904  isslmd  33172  isprmidl  33403  isprmidlc  33412  ismxidl  33427  ressply1mon1p  33531  isrrext  33984  ismntop  34010  isros  34152  issros  34159  issibf  34318  eulerpartleme  34348  eulerpartlemt0  34354  probun  34404  bnj250  34685  bnj255  34689  bnj345  34698  bnj945  34757  bnj1209  34780  bnj1275  34797  bnj543  34877  bnj571  34890  bnj607  34900  bnj882  34910  bnj983  34935  bnj996  34940  bnj1006  34944  bnj1033  34953  bnj1097  34965  bnj1110  34966  bnj1145  34977  bnj1174  34987  bnj1189  34993  bnj1450  35034  bnj1514  35047  wevgblacfn  35090  cusgr3cyclex  35117  erdszelem1  35172  cvmsval  35247  cvmliftiota  35282  snmlval  35312  lediv2aALT  35658  elwlim  35805  brtxp2  35863  brpprod3a  35868  brcart  35914  brsuccf  35923  broutsideof3  36108  ivthALT  36317  df3nandALT2  36382  andnand1  36383  topdifinffinlem  37329  relowlssretop  37345  rdgeqoa  37352  unccur  37591  fin2solem  37594  poimirlem3  37611  poimirlem4  37612  poimirlem26  37634  poimirlem27  37635  poimirlem32  37640  itg2gt0cn  37663  iblabsnclem  37671  areacirc  37701  neificl  37741  ablo4pnp  37868  isrngohom  37953  isidl  38002  ispridl  38022  pridlidl  38023  ismaxidl  38028  maxidlidl  38029  isfldidl2  38057  isdmn3  38062  triantru3  38212  moantr  38340  brxrn2  38351  dfxrn2  38352  ecxrn  38367  disjressuc2  38368  inxpxrn  38375  rnxrn  38378  dmqsblocks  38839  islshp  38966  isopos  39167  cvrfval  39255  cvrval  39256  isatl  39286  isat3  39294  islpln5  39523  4atlem11  39597  dalem20  39681  lhpexle3  40000  lhpex2leN  40001  isltrn2N  40108  diclspsn  41182  lcfls1lem  41522  lcfls1N  41523  uzindd  41959  isprimroot  42075  flt4lem5e  42638  3cubes  42672  fz1eqin  42751  dflim6  43247  dflim7  43256  nnoeomeqom  43295  cantnfub2  43305  fzunt  43438  fzuntd  43439  fzunt1d  43440  fzuntgd  43441  rp-isfinite6  43501  snhesn  43769  ismnuprim  44277  ismnushort  44284  iotasbc2  44403  eelT00  44688  eelTTT  44689  eelT11  44690  eelT12  44692  eelTT1  44693  eelT01  44694  eel0T1  44695  uun132  44768  uun132p1  44769  un2122  44773  uunTT1  44776  uunTT1p1  44777  uunTT1p2  44778  uunT11  44779  uunT11p1  44780  uunT11p2  44781  uunT12  44782  uunT12p1  44783  uunT12p2  44784  uunT12p3  44785  uunT12p4  44786  uunT12p5  44787  uun111  44788  uun2221  44796  uun2221p1  44797  uun2221p2  44798  stoweidlem17  46009  stoweidlem34  46026  stoweidlem60  46052  ndmaovass  47201  ndmaovdistr  47202  4an21  47265  2elfz3nn0  47311  difltmodne  47337  prproropf1o  47502  fpprel  47723  clnbgredg  47834  dfvopnbgr2  47847  dfclnbgr6  47850  dfnbgr6  47851  dfsclnbgr6  47852  uhgrimprop  47886  isuspgrimlem  47889  clnbgrgrim  47928  isgrtri  47936  isubgr3stgrlem4  47962  isubgr3stgrlem7  47965  upwlksfval  48117  isupwlkg  48119  upwlkbprop  48120  2zrngnmrid  48238  lindslinindsimp2lem5  48445  i0oii  48902  io1ii  48903  sepnsepolem1  48904  isthincd2  49420  functhinc  49431  elpg  49697  alimp-no-surprise  49764