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  3482  ceqsex2v  3483  ceqsex3v  3484  ceqsex4v  3485  ceqsex6v  3486  ceqsex8v  3487  2reu5lem1  3702  2reu5lem2  3703  2reu5lem3  3704  eldifpr  4603  rexdifpr  4604  trel3  5202  2rbropap  5514  ordelord  6341  dflim2  6377  dff1o4  6784  foco2  7057  brfvopab  7419  eloprabga  7471  ndmovass  7550  ndmovdistr  7551  dflim3  7793  dflim4  7794  frxp2  8089  mpoxopovel  8165  dfsmo2  8282  dfrecs3  8307  oeeui  8533  naddasslem2  8626  ecopovtrn  8762  elixp2  8844  elixp  8847  mptelixpg  8878  dif1en  9091  ssfi  9102  sbthfilem  9127  eqinf  9393  zorn2lem7  10419  grothprim  10752  grothtsk  10753  divmulasscom  11828  muldivdir  11842  divmuldiv  11850  sup3  12108  dfnn3  12183  prime  12605  eluz2  12789  raluz2  12842  elixx1  13302  elixx3g  13306  elioo2  13334  elioo5  13351  elicc4  13361  iccneg  13420  icoshft  13421  difreicc  13432  elfz1  13461  elfz  13462  elfz2  13463  elfzm11  13544  elfz2nn0  13567  elfzo2  13611  elfzo3  13626  lbfzo0  13649  fzo1lb  13663  1elfzo1  13664  fzind2  13738  zmodid2  13853  hashgt23el  14381  swrdnd2  14613  swrdnd0  14615  swrdccatin1  14682  swrdccat  14692  repswswrd  14741  swrdco  14794  2swrd2eqwrdeq  14910  rediv  15088  imdiv  15095  cosmul  16135  bitsval  16388  bitsmod  16400  bitscmp  16402  smueqlem  16454  dfgcd2  16510  lcmneg  16567  lcmftp  16600  coprmgcdb  16613  divgcdcoprmex  16630  cncongr1  16631  cncongr2  16632  difsqpwdvds  16853  oddprmdvds  16869  elgz  16897  xpsfrnel  17521  xpsfrnel2  17523  ismre  17547  mreexexlem4d  17608  iscatd2  17642  isssc  17782  eldmcoa  18027  isdrs  18262  isipodrs  18498  mgmsscl  18608  ismhm  18748  mhmpropd  18755  issubm  18766  issubmndb  18768  submacs  18790  issubg  19097  eqglact  19149  eqgid  19150  ecqusaddd  19162  ecqusaddcl  19163  pgrpsubgsymgbi  19378  isslw  19578  efgsdm  19700  mulgmhm  19797  mulgghm  19798  dmdprd  19970  dprdw  19982  subgdmdprd  20006  dmdprdpr  20021  isomnd  20093  isrng  20130  issrg  20164  srglmhm  20197  srgrmhm  20198  isring  20213  ringlghm  20288  dfrhm2  20449  issubrng  20519  issubrg3  20572  isdomn3  20687  issdrg  20760  sdrgacs  20773  islmod  20854  lsspropd  21008  islmhm  21018  islbs  21067  lbspropd  21090  qusmulrng  21276  rngqiprngghmlem3  21283  rngqiprnglinlem3  21287  rngqiprnglin  21296  cnfldfunALT  21363  cnfldfunALTOLD  21376  isphl  21622  elocv  21662  isobs  21714  mat1dimscm  22454  scmatghm  22512  scmatmhm  22513  ma1repvcl  22549  smadiadetr  22654  mat2pmatghm  22709  mat2pmatmul  22710  decpmatmulsumfsupp  22752  pm2mpghm  22795  pm2mpmhmlem1  22797  neindisj  23096  lmbrf  23239  hauscmplem  23385  llyi  23453  subislly  23460  islocfin  23496  uptx  23604  txcn  23605  qtopeu  23695  elmptrab  23806  isfbas  23808  trfil2  23866  flimcls  23964  cnextcn  24046  xmetec  24413  ngppropd  24616  ngpocelbl  24683  bl2ioo  24771  xrtgioo  24786  om1elbas  25013  elpi1  25026  isclm  25045  isclmp  25078  isncvsngp  25130  iscph  25151  tcphcph  25218  lmmbr2  25240  lmmbrf  25243  iscau2  25258  caussi  25278  lmclim  25284  bcthlem1  25305  srabn  25341  ishl2  25351  evthicc2  25441  ovolfioo  25448  ovolficc  25449  iblcnlem1  25769  iblrelem  25772  iblre  25775  iblcn  25780  isuc1p  26120  ismon1p  26122  ellogrn  26540  logreclem  26743  atandm  26857  atandm2  26858  atandm3  26859  atans2  26912  dmarea  26938  dchrelbas4  27224  lgsmodeq  27323  lgsmulsqcoprm  27324  nocvxminlem  27764  cutcuts  27791  cutbday  27794  addcuts2  27989  mulcut2  28143  ax5seg  29025  eengtrkg  29073  uspgredg2v  29311  nb3grpr2  29470  isrusgr0  29654  rusgrprop0  29655  ewlkprop  29691  wksfval  29697  wlkeq  29721  wlkson  29742  wlkonprop  29744  upgr2wlk  29754  upgrtrls  29787  upgristrl  29788  wksonproplem  29790  pthsfval  29806  ispth  29808  dfpth2  29816  isspthonpth  29836  uhgrwkspth  29842  usgr2wlkspth  29846  crctcshwlkn0lem4  29900  wspthnp  29937  wwlknon  29944  wwlksnextwrd  29984  wwlksnextinj  29986  wspthsnwspthsnon  30003  umgr2adedgwlk  30032  umgr2adedgwlkon  30033  umgr2adedgwlkonALT  30034  umgr2adedgspth  30035  s3wwlks2on  30043  sps3wwlks2on  30044  wpthswwlks2on  30051  usgr2wspthons3  30054  usgr2wspthon  30055  elwwlks2  30056  elwspths2spth  30057  rusgrnumwwlkl1  30058  rusgrnumwwlkslem  30059  isclwwlk  30073  clwwlkbp  30074  clwlkclwwlklem3  30090  isclwwlknx  30125  clwwlknp  30126  clwwlkn1  30130  clwwlkn2  30133  clwwlkwwlksb  30143  clwwlknonel  30184  0pth  30214  frcond4  30359  1to3vfriswmgr  30369  3cyclfrgr  30377  frgrwopreglem5  30410  2clwwlk2clwwlk  30439  numclwlk1lem1  30458  numclwwlk6  30479  ajval  30951  issh  31298  dmadjss  31977  adjeu  31979  adjval  31980  isst  32303  ishst  32304  xrdifh  32872  nndiffz1  32878  xdivpnfrp  33011  isslmd  33282  isprmidl  33517  isprmidlc  33526  ismxidl  33541  ressply1mon1p  33647  isrrext  34164  ismntop  34190  isros  34332  issros  34339  issibf  34497  eulerpartleme  34527  eulerpartlemt0  34533  probun  34583  bnj250  34864  bnj255  34868  bnj345  34877  bnj945  34936  bnj1209  34958  bnj1275  34975  bnj543  35055  bnj571  35068  bnj607  35078  bnj882  35088  bnj983  35113  bnj996  35118  bnj1006  35122  bnj1033  35131  bnj1097  35143  bnj1110  35144  bnj1145  35155  bnj1174  35165  bnj1189  35171  bnj1450  35212  bnj1514  35225  axprALT2  35273  wevgblacfn  35311  cusgr3cyclex  35338  erdszelem1  35393  cvmsval  35468  cvmliftiota  35503  snmlval  35533  lediv2aALT  35879  elwlim  36023  brtxp2  36081  brpprod3a  36086  brcart  36132  lemsuccf  36141  broutsideof3  36328  ivthALT  36537  df3nandALT2  36602  andnand1  36603  topdifinffinlem  37683  relowlssretop  37699  rdgeqoa  37706  unccur  37944  fin2solem  37947  poimirlem3  37964  poimirlem4  37965  poimirlem26  37987  poimirlem27  37988  poimirlem32  37993  itg2gt0cn  38016  iblabsnclem  38024  areacirc  38054  neificl  38094  ablo4pnp  38221  isrngohom  38306  isidl  38355  ispridl  38375  pridlidl  38376  ismaxidl  38381  maxidlidl  38382  isfldidl2  38410  isdmn3  38415  triantru3  38577  moantr  38713  brxrn2  38725  dfxrn2  38726  ecxrn  38747  disjressuc2  38752  inxpxrn  38759  rnxrn  38762  dfsuccl4  38815  dmqsblocks  39308  islshp  39445  isopos  39646  cvrfval  39734  cvrval  39735  isatl  39765  isat3  39773  islpln5  40001  4atlem11  40075  dalem20  40159  lhpexle3  40478  lhpex2leN  40479  isltrn2N  40586  diclspsn  41660  lcfls1lem  42000  lcfls1N  42001  uzindd  42437  isprimroot  42552  flt4lem5e  43109  3cubes  43142  fz1eqin  43221  dflim6  43716  dflim7  43725  nnoeomeqom  43764  cantnfub2  43774  fzunt  43906  fzuntd  43907  fzunt1d  43908  fzuntgd  43909  rp-isfinite6  43969  snhesn  44237  ismnuprim  44745  ismnushort  44752  iotasbc2  44871  eelT00  45155  eelTTT  45156  eelT11  45157  eelT12  45159  eelTT1  45160  eelT01  45161  eel0T1  45162  uun132  45235  uun132p1  45236  un2122  45240  uunTT1  45243  uunTT1p1  45244  uunTT1p2  45245  uunT11  45246  uunT11p1  45247  uunT11p2  45248  uunT12  45249  uunT12p1  45250  uunT12p2  45251  uunT12p3  45252  uunT12p4  45253  uunT12p5  45254  uun111  45255  uun2221  45263  uun2221p1  45264  uun2221p2  45265  stoweidlem17  46469  stoweidlem34  46486  stoweidlem60  46512  ndmaovass  47672  ndmaovdistr  47673  4an21  47736  2elfz3nn0  47782  difltmodne  47814  prproropf1o  47985  fpprel  48222  clnbgredg  48334  dfvopnbgr2  48347  dfclnbgr6  48350  dfnbgr6  48351  dfsclnbgr6  48352  uhgrimprop  48386  isuspgrimlem  48389  clnbgrgrim  48428  isgrtri  48437  isubgr3stgrlem4  48463  isubgr3stgrlem7  48466  upwlksfval  48629  isupwlkg  48631  upwlkbprop  48632  2zrngnmrid  48750  lindslinindsimp2lem5  48956  i0oii  49413  io1ii  49414  sepnsepolem1  49415  isthincd2  49930  functhinc  49941  elpg  50207  alimp-no-surprise  50274