Theorem 3anass 1097

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 1091	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		anass 472	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3	1, 2	bitri 278	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

Syntax hints:   ↔ wb 209   ∧ wa 399   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  3anan12  1098  3ancoma  1100  anandi3  1104  3biant1d  1480  an33rean  1485  an33reanOLD  1486  cad1  1624  3exdistr  1969  ceqsex2  3448  ceqsex2v  3449  ceqsex3v  3450  ceqsex4v  3451  ceqsex6v  3452  ceqsex8v  3453  2reu5lem1  3657  2reu5lem2  3658  2reu5lem3  3659  eldifpr  4559  rexdifpr  4560  trel3  5154  2rbropap  5430  ordelord  6213  dflim2  6247  dff1o4  6647  foco2  6904  brfvopab  7246  eloprabga  7296  ndmovass  7374  ndmovdistr  7375  dflim3  7604  dflim4  7605  mpoxopovel  7940  dfsmo2  8062  dfrecs3  8087  oeeui  8308  ecopovtrn  8480  elixp2  8560  elixp  8563  mptelixpg  8594  dif1en  8818  ssfi  8829  eqinf  9078  zorn2lem7  10081  grothprim  10413  grothtsk  10414  divmulasscom  11479  muldivdir  11490  divmuldiv  11497  sup3  11754  dfnn3  11809  prime  12223  eluz2  12409  raluz2  12458  elixx1  12909  elixx3g  12913  elioo2  12941  elioo5  12957  elicc4  12967  iccneg  13025  icoshft  13026  difreicc  13037  elfz1  13065  elfz  13066  elfz2  13067  elfzm11  13148  elfz2nn0  13168  elfzo2  13211  elfzo3  13224  lbfzo0  13247  fzind2  13325  zmodid2  13437  hashgt23el  13956  swrdnd2  14185  swrdnd0  14187  swrdccatin1  14255  swrdccat  14265  repswswrd  14314  swrdco  14367  2swrd2eqwrdeq  14483  ccat2s1fvwALTOLD  14487  rediv  14659  imdiv  14666  cosmul  15697  bitsval  15946  bitsmod  15958  bitscmp  15960  smueqlem  16012  dfgcd2  16069  lcmneg  16123  lcmftp  16156  coprmgcdb  16169  divgcdcoprmex  16186  cncongr1  16187  cncongr2  16188  difsqpwdvds  16403  oddprmdvds  16419  elgz  16447  xpsfrnel  17021  xpsfrnel2  17023  ismre  17047  mreexexlem4d  17104  iscatd2  17138  isssc  17279  eldmcoa  17525  isdrs  17762  isipodrs  17997  mgmsscl  18073  ismhm  18174  mhmpropd  18178  issubm  18184  issubmndb  18186  submacs  18207  issubg  18497  eqglact  18549  eqgid  18550  pgrpsubgsymgbi  18754  isslw  18951  efgsdm  19074  mulgmhm  19167  mulgghm  19168  dmdprd  19339  dprdw  19351  subgdmdprd  19375  dmdprdpr  19390  issrg  19476  srglmhm  19504  srgrmhm  19505  isring  19520  ringlghm  19576  dfrhm2  19691  issubrg3  19782  issdrg  19793  sdrgacs  19799  islmod  19857  lsspropd  20008  islmhm  20018  islbs  20067  lbspropd  20090  isphl  20544  elocv  20584  isobs  20636  mat1dimscm  21326  scmatghm  21384  scmatmhm  21385  ma1repvcl  21421  smadiadetr  21526  mat2pmatghm  21581  mat2pmatmul  21582  decpmatmulsumfsupp  21624  pm2mpghm  21667  pm2mpmhmlem1  21669  neindisj  21968  lmbrf  22111  hauscmplem  22257  llyi  22325  subislly  22332  islocfin  22368  uptx  22476  txcn  22477  qtopeu  22567  elmptrab  22678  isfbas  22680  trfil2  22738  flimcls  22836  cnextcn  22918  xmetec  23286  ngppropd  23489  ngpocelbl  23556  bl2ioo  23643  xrtgioo  23657  om1elbas  23883  elpi1  23896  isclm  23915  isclmp  23948  isncvsngp  24000  iscph  24021  tcphcph  24088  lmmbr2  24110  lmmbrf  24113  iscau2  24128  caussi  24148  lmclim  24154  bcthlem1  24175  srabn  24211  ishl2  24221  evthicc2  24311  ovolfioo  24318  ovolficc  24319  iblcnlem1  24639  iblrelem  24642  iblre  24645  iblcn  24650  isuc1p  24992  ismon1p  24994  ellogrn  25402  logreclem  25599  atandm  25713  atandm2  25714  atandm3  25715  atans2  25768  dmarea  25794  dchrelbas4  26078  lgsmodeq  26177  lgsmulsqcoprm  26178  ax5seg  26983  eengtrkg  27031  uspgredg2v  27266  nb3grpr2  27425  isrusgr0  27608  rusgrprop0  27609  ewlkprop  27645  wksfval  27651  wlkeq  27675  wlkson  27698  wlkonprop  27700  upgr2wlk  27710  upgrtrls  27743  upgristrl  27744  wksonproplem  27746  pthsfval  27762  ispth  27764  isspthonpth  27790  uhgrwkspth  27796  usgr2wlkspth  27800  crctcshwlkn0lem4  27851  wspthnp  27888  wwlknon  27895  wwlksnextwrd  27935  wwlksnextinj  27937  wspthsnwspthsnon  27954  umgr2adedgwlk  27983  umgr2adedgwlkon  27984  umgr2adedgwlkonALT  27985  umgr2adedgspth  27986  s3wwlks2on  27994  wpthswwlks2on  27999  usgr2wspthons3  28002  usgr2wspthon  28003  elwwlks2  28004  elwspths2spth  28005  rusgrnumwwlkl1  28006  rusgrnumwwlkslem  28007  isclwwlk  28021  clwwlkbp  28022  clwlkclwwlklem3  28038  isclwwlknx  28073  clwwlknp  28074  clwwlkn1  28078  clwwlkn2  28081  clwwlkwwlksb  28091  clwwlknonel  28132  0pth  28162  frcond4  28307  1to3vfriswmgr  28317  3cyclfrgr  28325  frgrwopreglem5  28358  2clwwlk2clwwlk  28387  numclwlk1lem1  28406  numclwwlk6  28427  ajval  28896  issh  29243  dmadjss  29922  adjeu  29924  adjval  29925  isst  30248  ishst  30249  xrdifh  30775  nndiffz1  30781  xdivpnfrp  30881  isomnd  31000  isslmd  31128  isprmidl  31281  isprmidlc  31291  ismxidl  31302  isrrext  31616  ismntop  31642  isros  31802  issros  31809  issibf  31966  eulerpartleme  31996  eulerpartlemt0  32002  probun  32052  bnj250  32346  bnj255  32350  bnj345  32359  bnj945  32420  bnj1209  32443  bnj1275  32460  bnj543  32540  bnj571  32553  bnj607  32563  bnj882  32573  bnj983  32598  bnj996  32603  bnj1006  32607  bnj1033  32616  bnj1097  32628  bnj1110  32629  bnj1145  32640  bnj1174  32650  bnj1189  32656  bnj1450  32697  bnj1514  32710  cusgr3cyclex  32765  erdszelem1  32820  cvmsval  32895  cvmliftiota  32930  snmlval  32960  lediv2aALT  33302  frxp2  33471  elwlim  33497  nocvxminlem  33658  scutcut  33681  scutbday  33684  brtxp2  33869  brpprod3a  33874  brcart  33920  brsuccf  33929  broutsideof3  34114  ivthALT  34210  df3nandALT2  34275  andnand1  34276  topdifinffinlem  35204  relowlssretop  35220  rdgeqoa  35227  unccur  35446  fin2solem  35449  poimirlem3  35466  poimirlem4  35467  poimirlem26  35489  poimirlem27  35490  poimirlem32  35495  itg2gt0cn  35518  iblabsnclem  35526  areacirc  35556  neificl  35597  ablo4pnp  35724  isrngohom  35809  isidl  35858  ispridl  35878  pridlidl  35879  ismaxidl  35884  maxidlidl  35885  isfldidl2  35913  isdmn3  35918  triantru3  36066  moantr  36180  brxrn2  36191  dfxrn2  36192  ecxrn  36203  inxpxrn  36207  rnxrn  36210  islshp  36679  isopos  36880  cvrfval  36968  cvrval  36969  isatl  36999  isat3  37007  islpln5  37235  4atlem11  37309  dalem20  37393  lhpexle3  37712  lhpex2leN  37713  isltrn2N  37820  diclspsn  38894  lcfls1lem  39234  lcfls1N  39235  uzindd  39668  flt4lem5e  40137  3cubes  40156  fz1eqin  40235  isdomn3  40673  rp-isfinite6  40751  snhesn  41012  ismnuprim  41526  ismnushort  41533  iotasbc2  41652  eelT00  41939  eelTTT  41940  eelT11  41941  eelT12  41943  eelTT1  41944  eelT01  41945  eel0T1  41946  uun132  42019  uun132p1  42020  un2122  42024  uunTT1  42027  uunTT1p1  42028  uunTT1p2  42029  uunT11  42030  uunT11p1  42031  uunT11p2  42032  uunT12  42033  uunT12p1  42034  uunT12p2  42035  uunT12p3  42036  uunT12p4  42037  uunT12p5  42038  uun111  42039  uun2221  42047  uun2221p1  42048  uun2221p2  42049  stoweidlem17  43176  stoweidlem34  43193  stoweidlem60  43219  ndmaovass  44313  ndmaovdistr  44314  4an21  44377  2elfz3nn0  44424  prproropf1o  44575  fpprel  44796  upwlksfval  44913  isupwlkg  44915  upwlkbprop  44916  isrng  45050  2zrngnmrid  45124  lindslinindsimp2lem5  45419  i0oii  45829  io1ii  45830  sepnsepolem1  45831  iscnrm3lem3  45845  isthincd2  45935  functhinc  45942  elpg  46033  alimp-no-surprise  46099