Theorem 3anass 1092

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 1086	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		anass 467	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3	1, 2	bitri 274	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

Syntax hints:   ↔ wb 205   ∧ wa 394   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  3anan12  1093  3ancoma  1095  anandi3  1099  3biant1d  1475  an33rean  1480  cad1  1611  3exdistr  1957  ceqsex2  3531  ceqsex2v  3532  ceqsex3v  3533  ceqsex4v  3534  ceqsex6v  3535  ceqsex8v  3536  2reu5lem1  3761  2reu5lem2  3762  2reu5lem3  3763  eldifpr  4668  rexdifpr  4669  trel3  5283  2rbropap  5576  ordelord  6402  dflim2  6437  dff1o4  6855  foco2  7128  brfvopab  7488  eloprabga  7539  ndmovass  7619  ndmovdistr  7620  dflim3  7865  dflim4  7866  frxp2  8166  mpoxopovel  8243  dfsmo2  8385  dfrecs3  8410  dfrecs3OLD  8411  oeeui  8640  naddasslem2  8733  ecopovtrn  8857  elixp2  8938  elixp  8941  mptelixpg  8972  dif1en  9205  dif1enOLD  9207  ssfi  9219  sbthfilem  9243  eqinf  9534  zorn2lem7  10552  grothprim  10884  grothtsk  10885  divmulasscom  11954  muldivdir  11968  divmuldiv  11975  sup3  12233  dfnn3  12288  prime  12705  eluz2  12890  raluz2  12943  elixx1  13397  elixx3g  13401  elioo2  13429  elioo5  13445  elicc4  13455  iccneg  13513  icoshft  13514  difreicc  13525  elfz1  13553  elfz  13554  elfz2  13555  elfzm11  13636  elfz2nn0  13656  elfzo2  13699  elfzo3  13713  lbfzo0  13736  fzind2  13815  zmodid2  13930  hashgt23el  14453  swrdnd2  14684  swrdnd0  14686  swrdccatin1  14754  swrdccat  14764  repswswrd  14813  swrdco  14867  2swrd2eqwrdeq  14983  rediv  15157  imdiv  15164  cosmul  16196  bitsval  16445  bitsmod  16457  bitscmp  16459  smueqlem  16511  dfgcd2  16568  lcmneg  16625  lcmftp  16658  coprmgcdb  16671  divgcdcoprmex  16688  cncongr1  16689  cncongr2  16690  difsqpwdvds  16910  oddprmdvds  16926  elgz  16954  xpsfrnel  17598  xpsfrnel2  17600  ismre  17624  mreexexlem4d  17681  iscatd2  17715  isssc  17857  eldmcoa  18108  isdrs  18347  isipodrs  18583  mgmsscl  18659  ismhm  18796  mhmpropd  18803  issubm  18814  issubmndb  18816  submacs  18838  issubg  19142  eqglact  19195  eqgid  19196  ecqusaddd  19208  ecqusaddcl  19209  pgrpsubgsymgbi  19428  isslw  19628  efgsdm  19750  mulgmhm  19847  mulgghm  19848  dmdprd  20020  dprdw  20032  subgdmdprd  20056  dmdprdpr  20071  isrng  20159  issrg  20193  srglmhm  20226  srgrmhm  20227  isring  20242  ringlghm  20313  dfrhm2  20478  issubrng  20551  issubrg3  20606  isdomn3  20715  issdrg  20789  sdrgacs  20802  islmod  20862  lsspropd  21017  islmhm  21027  islbs  21076  lbspropd  21099  qusmulrng  21293  rngqiprngghmlem3  21300  rngqiprnglinlem3  21304  rngqiprnglin  21313  cnfldfunALT  21380  cnfldfunALTOLD  21393  isphl  21646  elocv  21686  isobs  21740  mat1dimscm  22491  scmatghm  22549  scmatmhm  22550  ma1repvcl  22586  smadiadetr  22691  mat2pmatghm  22746  mat2pmatmul  22747  decpmatmulsumfsupp  22789  pm2mpghm  22832  pm2mpmhmlem1  22834  neindisj  23135  lmbrf  23278  hauscmplem  23424  llyi  23492  subislly  23499  islocfin  23535  uptx  23643  txcn  23644  qtopeu  23734  elmptrab  23845  isfbas  23847  trfil2  23905  flimcls  24003  cnextcn  24085  xmetec  24454  ngppropd  24660  ngpocelbl  24735  bl2ioo  24822  xrtgioo  24836  om1elbas  25073  elpi1  25086  isclm  25105  isclmp  25138  isncvsngp  25191  iscph  25212  tcphcph  25279  lmmbr2  25301  lmmbrf  25304  iscau2  25319  caussi  25339  lmclim  25345  bcthlem1  25366  srabn  25402  ishl2  25412  evthicc2  25503  ovolfioo  25510  ovolficc  25511  iblcnlem1  25831  iblrelem  25834  iblre  25837  iblcn  25842  isuc1p  26191  ismon1p  26193  ellogrn  26609  logreclem  26813  atandm  26927  atandm2  26928  atandm3  26929  atans2  26982  dmarea  27008  dchrelbas4  27295  lgsmodeq  27394  lgsmulsqcoprm  27395  nocvxminlem  27830  scutcut  27854  scutbday  27857  addscut2  28016  mulscut2  28157  ax5seg  28895  eengtrkg  28943  uspgredg2v  29183  nb3grpr2  29342  isrusgr0  29526  rusgrprop0  29527  ewlkprop  29563  wksfval  29569  wlkeq  29594  wlkson  29616  wlkonprop  29618  upgr2wlk  29628  upgrtrls  29661  upgristrl  29662  wksonproplem  29664  wksonproplemOLD  29665  pthsfval  29681  ispth  29683  isspthonpth  29709  uhgrwkspth  29715  usgr2wlkspth  29719  crctcshwlkn0lem4  29770  wspthnp  29807  wwlknon  29814  wwlksnextwrd  29854  wwlksnextinj  29856  wspthsnwspthsnon  29873  umgr2adedgwlk  29902  umgr2adedgwlkon  29903  umgr2adedgwlkonALT  29904  umgr2adedgspth  29905  s3wwlks2on  29913  wpthswwlks2on  29918  usgr2wspthons3  29921  usgr2wspthon  29922  elwwlks2  29923  elwspths2spth  29924  rusgrnumwwlkl1  29925  rusgrnumwwlkslem  29926  isclwwlk  29940  clwwlkbp  29941  clwlkclwwlklem3  29957  isclwwlknx  29992  clwwlknp  29993  clwwlkn1  29997  clwwlkn2  30000  clwwlkwwlksb  30010  clwwlknonel  30051  0pth  30081  frcond4  30226  1to3vfriswmgr  30236  3cyclfrgr  30244  frgrwopreglem5  30277  2clwwlk2clwwlk  30306  numclwlk1lem1  30325  numclwwlk6  30346  ajval  30817  issh  31164  dmadjss  31843  adjeu  31845  adjval  31846  isst  32169  ishst  32170  xrdifh  32710  nndiffz1  32716  xdivpnfrp  32822  isomnd  32965  isslmd  33095  isprmidl  33344  isprmidlc  33353  ismxidl  33368  ressply1mon1p  33471  isrrext  33853  ismntop  33879  isros  34039  issros  34046  issibf  34205  eulerpartleme  34235  eulerpartlemt0  34241  probun  34291  bnj250  34584  bnj255  34588  bnj345  34597  bnj945  34656  bnj1209  34679  bnj1275  34696  bnj543  34776  bnj571  34789  bnj607  34799  bnj882  34809  bnj983  34834  bnj996  34839  bnj1006  34843  bnj1033  34852  bnj1097  34864  bnj1110  34865  bnj1145  34876  bnj1174  34886  bnj1189  34892  bnj1450  34933  bnj1514  34946  wevgblacfn  34983  cusgr3cyclex  35011  erdszelem1  35066  cvmsval  35141  cvmliftiota  35176  snmlval  35206  lediv2aALT  35552  elwlim  35694  brtxp2  35752  brpprod3a  35757  brcart  35803  brsuccf  35812  broutsideof3  35997  ivthALT  36095  df3nandALT2  36160  andnand1  36161  topdifinffinlem  37101  relowlssretop  37117  rdgeqoa  37124  unccur  37351  fin2solem  37354  poimirlem3  37371  poimirlem4  37372  poimirlem26  37394  poimirlem27  37395  poimirlem32  37400  itg2gt0cn  37423  iblabsnclem  37431  areacirc  37461  neificl  37501  ablo4pnp  37628  isrngohom  37713  isidl  37762  ispridl  37782  pridlidl  37783  ismaxidl  37788  maxidlidl  37789  isfldidl2  37817  isdmn3  37822  triantru3  37973  moantr  38109  brxrn2  38120  dfxrn2  38121  ecxrn  38132  disjressuc2  38133  inxpxrn  38140  rnxrn  38143  islshp  38724  isopos  38925  cvrfval  39013  cvrval  39014  isatl  39044  isat3  39052  islpln5  39281  4atlem11  39355  dalem20  39439  lhpexle3  39758  lhpex2leN  39759  isltrn2N  39866  diclspsn  40940  lcfls1lem  41280  lcfls1N  41281  uzindd  41722  isprimroot  41839  flt4lem5e  42380  3cubes  42418  fz1eqin  42497  dflim6  43001  dflim7  43010  nnoeomeqom  43049  cantnfub2  43059  fzunt  43193  fzuntd  43194  fzunt1d  43195  fzuntgd  43196  rp-isfinite6  43256  snhesn  43524  ismnuprim  44039  ismnushort  44046  iotasbc2  44165  eelT00  44452  eelTTT  44453  eelT11  44454  eelT12  44456  eelTT1  44457  eelT01  44458  eel0T1  44459  uun132  44532  uun132p1  44533  un2122  44537  uunTT1  44540  uunTT1p1  44541  uunTT1p2  44542  uunT11  44543  uunT11p1  44544  uunT11p2  44545  uunT12  44546  uunT12p1  44547  uunT12p2  44548  uunT12p3  44549  uunT12p4  44550  uunT12p5  44551  uun111  44552  uun2221  44560  uun2221p1  44561  uun2221p2  44562  stoweidlem17  45708  stoweidlem34  45725  stoweidlem60  45751  ndmaovass  46889  ndmaovdistr  46890  4an21  46953  2elfz3nn0  46999  prproropf1o  47149  fpprel  47370  dfvopnbgr2  47490  dfclnbgr6  47493  dfnbgr6  47494  dfsclnbgr6  47495  uspgrimprop  47522  isuspgrimlem  47523  clnbgrgrim  47551  isgrtri  47586  upwlksfval  47593  isupwlkg  47595  upwlkbprop  47596  2zrngnmrid  47714  lindslinindsimp2lem5  47926  i0oii  48334  io1ii  48335  sepnsepolem1  48336  iscnrm3lem3  48350  isthincd2  48440  functhinc  48447  elpg  48541  alimp-no-surprise  48610