Theorem 3anass 1095

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 1089	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		anass 468	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3	1, 2	bitri 275	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  3anan12  1096  3ancoma  1098  anandi3  1102  4anpull2  1363  3biant1d  1481  an33rean  1486  cad1  1619  3exdistr  1962  ceqsex2  3481  ceqsex2v  3482  ceqsex3v  3483  ceqsex4v  3484  ceqsex6v  3485  ceqsex8v  3486  2reu5lem1  3701  2reu5lem2  3702  2reu5lem3  3703  eldifpr  4602  rexdifpr  4603  trel3  5201  2rbropap  5519  ordelord  6345  dflim2  6381  dff1o4  6788  foco2  7061  brfvopab  7424  eloprabga  7476  ndmovass  7555  ndmovdistr  7556  dflim3  7798  dflim4  7799  frxp2  8094  mpoxopovel  8170  dfsmo2  8287  dfrecs3  8312  oeeui  8538  naddasslem2  8631  ecopovtrn  8767  elixp2  8849  elixp  8852  mptelixpg  8883  dif1en  9096  ssfi  9107  sbthfilem  9132  eqinf  9398  zorn2lem7  10424  grothprim  10757  grothtsk  10758  divmulasscom  11833  muldivdir  11847  divmuldiv  11855  sup3  12113  dfnn3  12188  prime  12610  eluz2  12794  raluz2  12847  elixx1  13307  elixx3g  13311  elioo2  13339  elioo5  13356  elicc4  13366  iccneg  13425  icoshft  13426  difreicc  13437  elfz1  13466  elfz  13467  elfz2  13468  elfzm11  13549  elfz2nn0  13572  elfzo2  13616  elfzo3  13631  lbfzo0  13654  fzo1lb  13668  1elfzo1  13669  fzind2  13743  zmodid2  13858  hashgt23el  14386  swrdnd2  14618  swrdnd0  14620  swrdccatin1  14687  swrdccat  14697  repswswrd  14746  swrdco  14799  2swrd2eqwrdeq  14915  rediv  15093  imdiv  15100  cosmul  16140  bitsval  16393  bitsmod  16405  bitscmp  16407  smueqlem  16459  dfgcd2  16515  lcmneg  16572  lcmftp  16605  coprmgcdb  16618  divgcdcoprmex  16635  cncongr1  16636  cncongr2  16637  difsqpwdvds  16858  oddprmdvds  16874  elgz  16902  xpsfrnel  17526  xpsfrnel2  17528  ismre  17552  mreexexlem4d  17613  iscatd2  17647  isssc  17787  eldmcoa  18032  isdrs  18267  isipodrs  18503  mgmsscl  18613  ismhm  18753  mhmpropd  18760  issubm  18771  issubmndb  18773  submacs  18795  issubg  19102  eqglact  19154  eqgid  19155  ecqusaddd  19167  ecqusaddcl  19168  pgrpsubgsymgbi  19383  isslw  19583  efgsdm  19705  mulgmhm  19802  mulgghm  19803  dmdprd  19975  dprdw  19987  subgdmdprd  20011  dmdprdpr  20026  isomnd  20098  isrng  20135  issrg  20169  srglmhm  20202  srgrmhm  20203  isring  20218  ringlghm  20293  dfrhm2  20454  issubrng  20524  issubrg3  20577  isdomn3  20692  issdrg  20765  sdrgacs  20778  islmod  20859  lsspropd  21012  islmhm  21022  islbs  21071  lbspropd  21094  qusmulrng  21280  rngqiprngghmlem3  21287  rngqiprnglinlem3  21291  rngqiprnglin  21300  cnfldfunALT  21367  isphl  21608  elocv  21648  isobs  21700  mat1dimscm  22440  scmatghm  22498  scmatmhm  22499  ma1repvcl  22535  smadiadetr  22640  mat2pmatghm  22695  mat2pmatmul  22696  decpmatmulsumfsupp  22738  pm2mpghm  22781  pm2mpmhmlem1  22783  neindisj  23082  lmbrf  23225  hauscmplem  23371  llyi  23439  subislly  23446  islocfin  23482  uptx  23590  txcn  23591  qtopeu  23681  elmptrab  23792  isfbas  23794  trfil2  23852  flimcls  23950  cnextcn  24032  xmetec  24399  ngppropd  24602  ngpocelbl  24669  bl2ioo  24757  xrtgioo  24772  om1elbas  24999  elpi1  25012  isclm  25031  isclmp  25064  isncvsngp  25116  iscph  25137  tcphcph  25204  lmmbr2  25226  lmmbrf  25229  iscau2  25244  caussi  25264  lmclim  25270  bcthlem1  25291  srabn  25327  ishl2  25337  evthicc2  25427  ovolfioo  25434  ovolficc  25435  iblcnlem1  25755  iblrelem  25758  iblre  25761  iblcn  25766  isuc1p  26106  ismon1p  26108  ellogrn  26523  logreclem  26726  atandm  26840  atandm2  26841  atandm3  26842  atans2  26895  dmarea  26921  dchrelbas4  27206  lgsmodeq  27305  lgsmulsqcoprm  27306  nocvxminlem  27746  cutcuts  27773  cutbday  27776  addcuts2  27971  mulcut2  28125  ax5seg  29007  eengtrkg  29055  uspgredg2v  29293  nb3grpr2  29452  isrusgr0  29635  rusgrprop0  29636  ewlkprop  29672  wksfval  29678  wlkeq  29702  wlkson  29723  wlkonprop  29725  upgr2wlk  29735  upgrtrls  29768  upgristrl  29769  wksonproplem  29771  pthsfval  29787  ispth  29789  dfpth2  29797  isspthonpth  29817  uhgrwkspth  29823  usgr2wlkspth  29827  crctcshwlkn0lem4  29881  wspthnp  29918  wwlknon  29925  wwlksnextwrd  29965  wwlksnextinj  29967  wspthsnwspthsnon  29984  umgr2adedgwlk  30013  umgr2adedgwlkon  30014  umgr2adedgwlkonALT  30015  umgr2adedgspth  30016  s3wwlks2on  30024  sps3wwlks2on  30025  wpthswwlks2on  30032  usgr2wspthons3  30035  usgr2wspthon  30036  elwwlks2  30037  elwspths2spth  30038  rusgrnumwwlkl1  30039  rusgrnumwwlkslem  30040  isclwwlk  30054  clwwlkbp  30055  clwlkclwwlklem3  30071  isclwwlknx  30106  clwwlknp  30107  clwwlkn1  30111  clwwlkn2  30114  clwwlkwwlksb  30124  clwwlknonel  30165  0pth  30195  frcond4  30340  1to3vfriswmgr  30350  3cyclfrgr  30358  frgrwopreglem5  30391  2clwwlk2clwwlk  30420  numclwlk1lem1  30439  numclwwlk6  30460  ajval  30932  issh  31279  dmadjss  31958  adjeu  31960  adjval  31961  isst  32284  ishst  32285  xrdifh  32853  nndiffz1  32859  xdivpnfrp  32992  isslmd  33263  isprmidl  33498  isprmidlc  33507  ismxidl  33522  ressply1mon1p  33628  isrrext  34144  ismntop  34170  isros  34312  issros  34319  issibf  34477  eulerpartleme  34507  eulerpartlemt0  34513  probun  34563  bnj250  34844  bnj255  34848  bnj345  34857  bnj945  34916  bnj1209  34938  bnj1275  34955  bnj543  35035  bnj571  35048  bnj607  35058  bnj882  35068  bnj983  35093  bnj996  35098  bnj1006  35102  bnj1033  35111  bnj1097  35123  bnj1110  35124  bnj1145  35135  bnj1174  35145  bnj1189  35151  bnj1450  35192  bnj1514  35205  axprALT2  35253  wevgblacfn  35291  cusgr3cyclex  35318  erdszelem1  35373  cvmsval  35448  cvmliftiota  35483  snmlval  35513  lediv2aALT  35859  elwlim  36003  brtxp2  36061  brpprod3a  36066  brcart  36112  lemsuccf  36121  broutsideof3  36308  ivthALT  36517  df3nandALT2  36582  andnand1  36583  topdifinffinlem  37663  relowlssretop  37679  rdgeqoa  37686  unccur  37924  fin2solem  37927  poimirlem3  37944  poimirlem4  37945  poimirlem26  37967  poimirlem27  37968  poimirlem32  37973  itg2gt0cn  37996  iblabsnclem  38004  areacirc  38034  neificl  38074  ablo4pnp  38201  isrngohom  38286  isidl  38335  ispridl  38355  pridlidl  38356  ismaxidl  38361  maxidlidl  38362  isfldidl2  38390  isdmn3  38395  triantru3  38557  moantr  38693  brxrn2  38705  dfxrn2  38706  ecxrn  38727  disjressuc2  38732  inxpxrn  38739  rnxrn  38742  dfsuccl4  38795  dmqsblocks  39288  islshp  39425  isopos  39626  cvrfval  39714  cvrval  39715  isatl  39745  isat3  39753  islpln5  39981  4atlem11  40055  dalem20  40139  lhpexle3  40458  lhpex2leN  40459  isltrn2N  40566  diclspsn  41640  lcfls1lem  41980  lcfls1N  41981  uzindd  42417  isprimroot  42532  flt4lem5e  43089  3cubes  43122  fz1eqin  43201  dflim6  43692  dflim7  43701  nnoeomeqom  43740  cantnfub2  43750  fzunt  43882  fzuntd  43883  fzunt1d  43884  fzuntgd  43885  rp-isfinite6  43945  snhesn  44213  ismnuprim  44721  ismnushort  44728  iotasbc2  44847  eelT00  45131  eelTTT  45132  eelT11  45133  eelT12  45135  eelTT1  45136  eelT01  45137  eel0T1  45138  uun132  45211  uun132p1  45212  un2122  45216  uunTT1  45219  uunTT1p1  45220  uunTT1p2  45221  uunT11  45222  uunT11p1  45223  uunT11p2  45224  uunT12  45225  uunT12p1  45226  uunT12p2  45227  uunT12p3  45228  uunT12p4  45229  uunT12p5  45230  uun111  45231  uun2221  45239  uun2221p1  45240  uun2221p2  45241  stoweidlem17  46445  stoweidlem34  46462  stoweidlem60  46488  ndmaovass  47654  ndmaovdistr  47655  4an21  47718  2elfz3nn0  47764  difltmodne  47796  prproropf1o  47967  fpprel  48204  clnbgredg  48316  dfvopnbgr2  48329  dfclnbgr6  48332  dfnbgr6  48333  dfsclnbgr6  48334  uhgrimprop  48368  isuspgrimlem  48371  clnbgrgrim  48410  isgrtri  48419  isubgr3stgrlem4  48445  isubgr3stgrlem7  48448  upwlksfval  48611  isupwlkg  48613  upwlkbprop  48614  2zrngnmrid  48732  lindslinindsimp2lem5  48938  i0oii  49395  io1ii  49396  sepnsepolem1  49397  isthincd2  49912  functhinc  49923  elpg  50189  alimp-no-surprise  50256