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  10431  grothprim  10763  grothtsk  10764  divmulasscom  11837  muldivdir  11851  divmuldiv  11858  sup3  12116  dfnn3  12176  prime  12591  eluz2  12775  raluz2  12832  elixx1  13291  elixx3g  13295  elioo2  13323  elioo5  13340  elicc4  13350  iccneg  13409  icoshft  13410  difreicc  13421  elfz1  13449  elfz  13450  elfz2  13451  elfzm11  13532  elfz2nn0  13555  elfzo2  13599  elfzo3  13613  lbfzo0  13636  fzo1lb  13650  1elfzo1  13651  fzind2  13722  zmodid2  13837  hashgt23el  14365  swrdnd2  14596  swrdnd0  14598  swrdccatin1  14666  swrdccat  14676  repswswrd  14725  swrdco  14779  2swrd2eqwrdeq  14895  rediv  15073  imdiv  15080  cosmul  16117  bitsval  16370  bitsmod  16382  bitscmp  16384  smueqlem  16436  dfgcd2  16492  lcmneg  16549  lcmftp  16582  coprmgcdb  16595  divgcdcoprmex  16612  cncongr1  16613  cncongr2  16614  difsqpwdvds  16834  oddprmdvds  16850  elgz  16878  xpsfrnel  17501  xpsfrnel2  17503  ismre  17527  mreexexlem4d  17588  iscatd2  17622  isssc  17762  eldmcoa  18007  isdrs  18242  isipodrs  18478  mgmsscl  18554  ismhm  18694  mhmpropd  18701  issubm  18712  issubmndb  18714  submacs  18736  issubg  19040  eqglact  19093  eqgid  19094  ecqusaddd  19106  ecqusaddcl  19107  pgrpsubgsymgbi  19322  isslw  19522  efgsdm  19644  mulgmhm  19741  mulgghm  19742  dmdprd  19914  dprdw  19926  subgdmdprd  19950  dmdprdpr  19965  isomnd  20037  isrng  20074  issrg  20108  srglmhm  20141  srgrmhm  20142  isring  20157  ringlghm  20232  dfrhm2  20394  issubrng  20467  issubrg3  20520  isdomn3  20635  issdrg  20708  sdrgacs  20721  islmod  20802  lsspropd  20956  islmhm  20966  islbs  21015  lbspropd  21038  qusmulrng  21224  rngqiprngghmlem3  21231  rngqiprnglinlem3  21235  rngqiprnglin  21244  cnfldfunALT  21311  cnfldfunALTOLD  21324  isphl  21570  elocv  21610  isobs  21662  mat1dimscm  22395  scmatghm  22453  scmatmhm  22454  ma1repvcl  22490  smadiadetr  22595  mat2pmatghm  22650  mat2pmatmul  22651  decpmatmulsumfsupp  22693  pm2mpghm  22736  pm2mpmhmlem1  22738  neindisj  23037  lmbrf  23180  hauscmplem  23326  llyi  23394  subislly  23401  islocfin  23437  uptx  23545  txcn  23546  qtopeu  23636  elmptrab  23747  isfbas  23749  trfil2  23807  flimcls  23905  cnextcn  23987  xmetec  24355  ngppropd  24558  ngpocelbl  24625  bl2ioo  24713  xrtgioo  24728  om1elbas  24965  elpi1  24978  isclm  24997  isclmp  25030  isncvsngp  25082  iscph  25103  tcphcph  25170  lmmbr2  25192  lmmbrf  25195  iscau2  25210  caussi  25230  lmclim  25236  bcthlem1  25257  srabn  25293  ishl2  25303  evthicc2  25394  ovolfioo  25401  ovolficc  25402  iblcnlem1  25722  iblrelem  25725  iblre  25728  iblcn  25733  isuc1p  26079  ismon1p  26081  ellogrn  26501  logreclem  26705  atandm  26819  atandm2  26820  atandm3  26821  atans2  26874  dmarea  26900  dchrelbas4  27187  lgsmodeq  27286  lgsmulsqcoprm  27287  nocvxminlem  27723  scutcut  27747  scutbday  27750  addscut2  27926  mulscut2  28076  ax5seg  28918  eengtrkg  28966  uspgredg2v  29204  nb3grpr2  29363  isrusgr0  29547  rusgrprop0  29548  ewlkprop  29584  wksfval  29590  wlkeq  29614  wlkson  29635  wlkonprop  29637  upgr2wlk  29647  upgrtrls  29680  upgristrl  29681  wksonproplem  29683  pthsfval  29699  ispth  29701  dfpth2  29709  isspthonpth  29729  uhgrwkspth  29735  usgr2wlkspth  29739  crctcshwlkn0lem4  29793  wspthnp  29830  wwlknon  29837  wwlksnextwrd  29877  wwlksnextinj  29879  wspthsnwspthsnon  29896  umgr2adedgwlk  29925  umgr2adedgwlkon  29926  umgr2adedgwlkonALT  29927  umgr2adedgspth  29928  s3wwlks2on  29936  wpthswwlks2on  29941  usgr2wspthons3  29944  usgr2wspthon  29945  elwwlks2  29946  elwspths2spth  29947  rusgrnumwwlkl1  29948  rusgrnumwwlkslem  29949  isclwwlk  29963  clwwlkbp  29964  clwlkclwwlklem3  29980  isclwwlknx  30015  clwwlknp  30016  clwwlkn1  30020  clwwlkn2  30023  clwwlkwwlksb  30033  clwwlknonel  30074  0pth  30104  frcond4  30249  1to3vfriswmgr  30259  3cyclfrgr  30267  frgrwopreglem5  30300  2clwwlk2clwwlk  30329  numclwlk1lem1  30348  numclwwlk6  30369  ajval  30840  issh  31187  dmadjss  31866  adjeu  31868  adjval  31869  isst  32192  ishst  32193  xrdifh  32753  nndiffz1  32759  xdivpnfrp  32903  isslmd  33171  isprmidl  33402  isprmidlc  33411  ismxidl  33426  ressply1mon1p  33530  isrrext  33983  ismntop  34009  isros  34151  issros  34158  issibf  34317  eulerpartleme  34347  eulerpartlemt0  34353  probun  34403  bnj250  34684  bnj255  34688  bnj345  34697  bnj945  34756  bnj1209  34779  bnj1275  34796  bnj543  34876  bnj571  34889  bnj607  34899  bnj882  34909  bnj983  34934  bnj996  34939  bnj1006  34943  bnj1033  34952  bnj1097  34964  bnj1110  34965  bnj1145  34976  bnj1174  34986  bnj1189  34992  bnj1450  35033  bnj1514  35046  wevgblacfn  35089  cusgr3cyclex  35116  erdszelem1  35171  cvmsval  35246  cvmliftiota  35281  snmlval  35311  lediv2aALT  35657  elwlim  35804  brtxp2  35862  brpprod3a  35867  brcart  35913  brsuccf  35922  broutsideof3  36107  ivthALT  36316  df3nandALT2  36381  andnand1  36382  topdifinffinlem  37328  relowlssretop  37344  rdgeqoa  37351  unccur  37590  fin2solem  37593  poimirlem3  37610  poimirlem4  37611  poimirlem26  37633  poimirlem27  37634  poimirlem32  37639  itg2gt0cn  37662  iblabsnclem  37670  areacirc  37700  neificl  37740  ablo4pnp  37867  isrngohom  37952  isidl  38001  ispridl  38021  pridlidl  38022  ismaxidl  38027  maxidlidl  38028  isfldidl2  38056  isdmn3  38061  triantru3  38211  moantr  38339  brxrn2  38350  dfxrn2  38351  ecxrn  38366  disjressuc2  38367  inxpxrn  38374  rnxrn  38377  dmqsblocks  38838  islshp  38965  isopos  39166  cvrfval  39254  cvrval  39255  isatl  39285  isat3  39293  islpln5  39522  4atlem11  39596  dalem20  39680  lhpexle3  39999  lhpex2leN  40000  isltrn2N  40107  diclspsn  41181  lcfls1lem  41521  lcfls1N  41522  uzindd  41958  isprimroot  42074  flt4lem5e  42637  3cubes  42671  fz1eqin  42750  dflim6  43246  dflim7  43255  nnoeomeqom  43294  cantnfub2  43304  fzunt  43437  fzuntd  43438  fzunt1d  43439  fzuntgd  43440  rp-isfinite6  43500  snhesn  43768  ismnuprim  44276  ismnushort  44283  iotasbc2  44402  eelT00  44687  eelTTT  44688  eelT11  44689  eelT12  44691  eelTT1  44692  eelT01  44693  eel0T1  44694  uun132  44767  uun132p1  44768  un2122  44772  uunTT1  44775  uunTT1p1  44776  uunTT1p2  44777  uunT11  44778  uunT11p1  44779  uunT11p2  44780  uunT12  44781  uunT12p1  44782  uunT12p2  44783  uunT12p3  44784  uunT12p4  44785  uunT12p5  44786  uun111  44787  uun2221  44795  uun2221p1  44796  uun2221p2  44797  stoweidlem17  46008  stoweidlem34  46025  stoweidlem60  46051  ndmaovass  47200  ndmaovdistr  47201  4an21  47264  2elfz3nn0  47310  difltmodne  47336  prproropf1o  47501  fpprel  47722  clnbgredg  47833  dfvopnbgr2  47846  dfclnbgr6  47849  dfnbgr6  47850  dfsclnbgr6  47851  uhgrimprop  47885  isuspgrimlem  47888  clnbgrgrim  47927  isgrtri  47935  isubgr3stgrlem4  47961  isubgr3stgrlem7  47964  upwlksfval  48116  isupwlkg  48118  upwlkbprop  48119  2zrngnmrid  48237  lindslinindsimp2lem5  48444  i0oii  48901  io1ii  48902  sepnsepolem1  48903  isthincd2  49419  functhinc  49430  elpg  49696  alimp-no-surprise  49763