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  3487  ceqsex2v  3488  ceqsex3v  3489  ceqsex4v  3490  ceqsex6v  3491  ceqsex8v  3492  2reu5lem1  3711  2reu5lem2  3712  2reu5lem3  3713  eldifpr  4608  rexdifpr  4609  trel3  5204  2rbropap  5501  ordelord  6323  dflim2  6359  dff1o4  6766  foco2  7036  brfvopab  7397  eloprabga  7449  ndmovass  7528  ndmovdistr  7529  dflim3  7771  dflim4  7772  frxp2  8068  mpoxopovel  8144  dfsmo2  8261  dfrecs3  8286  oeeui  8511  naddasslem2  8604  ecopovtrn  8738  elixp2  8819  elixp  8822  mptelixpg  8853  dif1en  9065  ssfi  9076  sbthfilem  9101  eqinf  9363  zorn2lem7  10384  grothprim  10716  grothtsk  10717  divmulasscom  11791  muldivdir  11805  divmuldiv  11812  sup3  12070  dfnn3  12130  prime  12545  eluz2  12729  raluz2  12786  elixx1  13245  elixx3g  13249  elioo2  13277  elioo5  13294  elicc4  13304  iccneg  13363  icoshft  13364  difreicc  13375  elfz1  13403  elfz  13404  elfz2  13405  elfzm11  13486  elfz2nn0  13509  elfzo2  13553  elfzo3  13567  lbfzo0  13590  fzo1lb  13604  1elfzo1  13605  fzind2  13676  zmodid2  13791  hashgt23el  14319  swrdnd2  14550  swrdnd0  14552  swrdccatin1  14619  swrdccat  14629  repswswrd  14678  swrdco  14731  2swrd2eqwrdeq  14847  rediv  15025  imdiv  15032  cosmul  16069  bitsval  16322  bitsmod  16334  bitscmp  16336  smueqlem  16388  dfgcd2  16444  lcmneg  16501  lcmftp  16534  coprmgcdb  16547  divgcdcoprmex  16564  cncongr1  16565  cncongr2  16566  difsqpwdvds  16786  oddprmdvds  16802  elgz  16830  xpsfrnel  17453  xpsfrnel2  17455  ismre  17479  mreexexlem4d  17540  iscatd2  17574  isssc  17714  eldmcoa  17959  isdrs  18194  isipodrs  18430  mgmsscl  18506  ismhm  18646  mhmpropd  18653  issubm  18664  issubmndb  18666  submacs  18688  issubg  18992  eqglact  19045  eqgid  19046  ecqusaddd  19058  ecqusaddcl  19059  pgrpsubgsymgbi  19274  isslw  19474  efgsdm  19596  mulgmhm  19693  mulgghm  19694  dmdprd  19866  dprdw  19878  subgdmdprd  19902  dmdprdpr  19917  isomnd  19989  isrng  20026  issrg  20060  srglmhm  20093  srgrmhm  20094  isring  20109  ringlghm  20184  dfrhm2  20346  issubrng  20416  issubrg3  20469  isdomn3  20584  issdrg  20657  sdrgacs  20670  islmod  20751  lsspropd  20905  islmhm  20915  islbs  20964  lbspropd  20987  qusmulrng  21173  rngqiprngghmlem3  21180  rngqiprnglinlem3  21184  rngqiprnglin  21193  cnfldfunALT  21260  cnfldfunALTOLD  21273  isphl  21519  elocv  21559  isobs  21611  mat1dimscm  22344  scmatghm  22402  scmatmhm  22403  ma1repvcl  22439  smadiadetr  22544  mat2pmatghm  22599  mat2pmatmul  22600  decpmatmulsumfsupp  22642  pm2mpghm  22685  pm2mpmhmlem1  22687  neindisj  22986  lmbrf  23129  hauscmplem  23275  llyi  23343  subislly  23350  islocfin  23386  uptx  23494  txcn  23495  qtopeu  23585  elmptrab  23696  isfbas  23698  trfil2  23756  flimcls  23854  cnextcn  23936  xmetec  24303  ngppropd  24506  ngpocelbl  24573  bl2ioo  24661  xrtgioo  24676  om1elbas  24913  elpi1  24926  isclm  24945  isclmp  24978  isncvsngp  25030  iscph  25051  tcphcph  25118  lmmbr2  25140  lmmbrf  25143  iscau2  25158  caussi  25178  lmclim  25184  bcthlem1  25205  srabn  25241  ishl2  25251  evthicc2  25342  ovolfioo  25349  ovolficc  25350  iblcnlem1  25670  iblrelem  25673  iblre  25676  iblcn  25681  isuc1p  26027  ismon1p  26029  ellogrn  26449  logreclem  26653  atandm  26767  atandm2  26768  atandm3  26769  atans2  26822  dmarea  26848  dchrelbas4  27135  lgsmodeq  27234  lgsmulsqcoprm  27235  nocvxminlem  27671  scutcut  27696  scutbday  27699  addscut2  27876  mulscut2  28026  ax5seg  28870  eengtrkg  28918  uspgredg2v  29156  nb3grpr2  29315  isrusgr0  29499  rusgrprop0  29500  ewlkprop  29536  wksfval  29542  wlkeq  29566  wlkson  29587  wlkonprop  29589  upgr2wlk  29599  upgrtrls  29632  upgristrl  29633  wksonproplem  29635  pthsfval  29651  ispth  29653  dfpth2  29661  isspthonpth  29681  uhgrwkspth  29687  usgr2wlkspth  29691  crctcshwlkn0lem4  29745  wspthnp  29782  wwlknon  29789  wwlksnextwrd  29829  wwlksnextinj  29831  wspthsnwspthsnon  29848  umgr2adedgwlk  29877  umgr2adedgwlkon  29878  umgr2adedgwlkonALT  29879  umgr2adedgspth  29880  s3wwlks2on  29888  wpthswwlks2on  29893  usgr2wspthons3  29896  usgr2wspthon  29897  elwwlks2  29898  elwspths2spth  29899  rusgrnumwwlkl1  29900  rusgrnumwwlkslem  29901  isclwwlk  29915  clwwlkbp  29916  clwlkclwwlklem3  29932  isclwwlknx  29967  clwwlknp  29968  clwwlkn1  29972  clwwlkn2  29975  clwwlkwwlksb  29985  clwwlknonel  30026  0pth  30056  frcond4  30201  1to3vfriswmgr  30211  3cyclfrgr  30219  frgrwopreglem5  30252  2clwwlk2clwwlk  30281  numclwlk1lem1  30300  numclwwlk6  30321  ajval  30792  issh  31139  dmadjss  31818  adjeu  31820  adjval  31821  isst  32144  ishst  32145  xrdifh  32715  nndiffz1  32721  xdivpnfrp  32868  isslmd  33139  isprmidl  33371  isprmidlc  33380  ismxidl  33395  ressply1mon1p  33499  isrrext  33981  ismntop  34007  isros  34149  issros  34156  issibf  34314  eulerpartleme  34344  eulerpartlemt0  34350  probun  34400  bnj250  34681  bnj255  34685  bnj345  34694  bnj945  34753  bnj1209  34776  bnj1275  34793  bnj543  34873  bnj571  34886  bnj607  34896  bnj882  34906  bnj983  34931  bnj996  34936  bnj1006  34940  bnj1033  34949  bnj1097  34961  bnj1110  34962  bnj1145  34973  bnj1174  34983  bnj1189  34989  bnj1450  35030  bnj1514  35043  wevgblacfn  35099  cusgr3cyclex  35126  erdszelem1  35181  cvmsval  35256  cvmliftiota  35291  snmlval  35321  lediv2aALT  35667  elwlim  35814  brtxp2  35872  brpprod3a  35877  brcart  35923  brsuccf  35932  broutsideof3  36117  ivthALT  36326  df3nandALT2  36391  andnand1  36392  topdifinffinlem  37338  relowlssretop  37354  rdgeqoa  37361  unccur  37600  fin2solem  37603  poimirlem3  37620  poimirlem4  37621  poimirlem26  37643  poimirlem27  37644  poimirlem32  37649  itg2gt0cn  37672  iblabsnclem  37680  areacirc  37710  neificl  37750  ablo4pnp  37877  isrngohom  37962  isidl  38011  ispridl  38031  pridlidl  38032  ismaxidl  38037  maxidlidl  38038  isfldidl2  38066  isdmn3  38071  triantru3  38221  moantr  38349  brxrn2  38360  dfxrn2  38361  ecxrn  38376  disjressuc2  38377  inxpxrn  38384  rnxrn  38387  dmqsblocks  38848  islshp  38975  isopos  39176  cvrfval  39264  cvrval  39265  isatl  39295  isat3  39303  islpln5  39531  4atlem11  39605  dalem20  39689  lhpexle3  40008  lhpex2leN  40009  isltrn2N  40116  diclspsn  41190  lcfls1lem  41530  lcfls1N  41531  uzindd  41967  isprimroot  42083  flt4lem5e  42646  3cubes  42680  fz1eqin  42759  dflim6  43254  dflim7  43263  nnoeomeqom  43302  cantnfub2  43312  fzunt  43445  fzuntd  43446  fzunt1d  43447  fzuntgd  43448  rp-isfinite6  43508  snhesn  43776  ismnuprim  44284  ismnushort  44291  iotasbc2  44410  eelT00  44694  eelTTT  44695  eelT11  44696  eelT12  44698  eelTT1  44699  eelT01  44700  eel0T1  44701  uun132  44774  uun132p1  44775  un2122  44779  uunTT1  44782  uunTT1p1  44783  uunTT1p2  44784  uunT11  44785  uunT11p1  44786  uunT11p2  44787  uunT12  44788  uunT12p1  44789  uunT12p2  44790  uunT12p3  44791  uunT12p4  44792  uunT12p5  44793  uun111  44794  uun2221  44802  uun2221p1  44803  uun2221p2  44804  stoweidlem17  46012  stoweidlem34  46029  stoweidlem60  46055  ndmaovass  47204  ndmaovdistr  47205  4an21  47268  2elfz3nn0  47314  difltmodne  47340  prproropf1o  47505  fpprel  47726  clnbgredg  47838  dfvopnbgr2  47851  dfclnbgr6  47854  dfnbgr6  47855  dfsclnbgr6  47856  uhgrimprop  47890  isuspgrimlem  47893  clnbgrgrim  47932  isgrtri  47941  isubgr3stgrlem4  47967  isubgr3stgrlem7  47970  upwlksfval  48133  isupwlkg  48135  upwlkbprop  48136  2zrngnmrid  48254  lindslinindsimp2lem5  48461  i0oii  48918  io1ii  48919  sepnsepolem1  48920  isthincd2  49436  functhinc  49447  elpg  49713  alimp-no-surprise  49780