Theorem 3anass 1111

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

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anan12  1112  3ancoma  1115  anandi3  1119  4anpull2OLD  1383  3biant1d  1509  an33rean  1514  cad1  1649  3exdistr  1992  ceqsex2  3500  ceqsex2v  3501  ceqsex3v  3502  ceqsex4v  3503  ceqsex6v  3504  ceqsex8v  3505  2reu5lem1  3712  2reu5lem2  3713  2reu5lem3  3714  eldifpr  4618  rexdifpr  4619  trel3  5220  2rbropap  5538  ordelord  6384  dflim2  6421  dff1o4  6833  foco2  7109  brfvopab  7477  eloprabga  7529  ndmovass  7609  ndmovdistr  7610  dflim3  7858  dflim4  7859  frxp2  8161  mpoxopovel  8237  dfsmo2  8355  dfrecs3  8380  oeeui  8611  naddasslem2  8705  ecopovtrn  8841  elixp2  8929  elixp  8932  mptelixpg  8963  dif1en  9177  ssfi  9188  sbthfilem  9213  eqinf  9477  zorn2lem7  10580  grothprim  10919  grothtsk  10920  divmulasscom  11998  muldivdir  12009  divmuldiv  12017  sup3  12274  dfnn3  12349  prime  12780  eluz2  12971  raluz2  13024  elixx1  13485  elixx3g  13489  elioo2  13517  elioo5  13534  elicc4  13544  iccneg  13603  icoshft  13604  difreicc  13615  elfz1  13644  elfz  13645  elfz2  13646  elfzm11  13729  elfz2nn0  13752  elfzo2  13796  elfzo3  13811  lbfzo0  13834  fzo1lb  13848  1elfzo1  13849  fzind2  13923  zmodid2  14039  hashgt23el  14569  swrdnd2  14805  swrdnd0  14807  swrdccatin1  14874  swrdccat  14884  repswswrd  14935  swrdco  14988  2swrd2eqwrdeq  15106  rediv  15298  imdiv  15305  cosmul  16341  bitsval  16594  bitsmod  16606  bitscmp  16608  smueqlem  16660  dfgcd2  16719  lcmneg  16778  lcmftp  16811  coprmgcdb  16824  divgcdcoprmex  16841  cncongr1  16842  cncongr2  16843  difsqpwdvds  17065  oddprmdvds  17081  elgz  17109  xpsfrnel  17734  xpsfrnel2  17736  ismre  17760  mreexexlem4d  17821  iscatd2  17855  isssc  17995  eldmcoa  18240  isdrs  18475  isipodrs  18711  mgmsscl  18821  ismhm  18980  mhmpropd  18987  issubm  18998  issubmndb  19000  submacs  19023  issubg  19336  eqglact  19391  eqgid  19392  ecqusaddd  19407  ecqusaddcl  19408  pgrpsubgsymgbi  19622  isslw  19822  efgsdm  19944  mulgmhm  20041  mulgghm  20042  dmdprd  20214  dprdw  20226  subgdmdprd  20250  dmdprdpr  20265  isomnd  20337  isrng  20376  issrg  20414  srglmhm  20447  srgrmhm  20448  isring  20463  dfring3  20518  ringlghm  20543  dfrhm2  20704  isrhm0  20706  crngrhmfo  20726  issubrng  20799  issubrg3  20852  isdomn3  20966  isdrng3  21007  issdrg  21045  sdrgacs  21058  islmod  21139  lsspropd  21292  islmhm  21302  islbs  21351  lbspropd  21374  isfieldidl  21540  isfieldidl2  21541  qusmulrng  21578  rngqiprngghmlem3  21585  rngqiprnglinlem3  21589  rngqiprnglin  21598  isprmidl  21619  isprmidlc  21628  cnfldfunALT  21693  isphl  21934  elocv  21974  isobs  22026  mat1dimscm  22790  scmatghm  22848  scmatmhm  22849  ma1repvcl  22885  smadiadetr  22990  mat2pmatghm  23048  mat2pmatmul  23049  decpmatmulsumfsupp  23091  pm2mpghm  23134  pm2mpmhmlem1  23136  neindisj  23435  lmbrf  23578  hauscmplem  23724  llyi  23793  subislly  23800  islocfin  23836  uptx  23944  txcn  23945  qtopeu  24035  elmptrab  24146  isfbas  24148  trfil2  24206  flimcls  24304  cnextcn  24386  xmetec  24753  ngppropd  24956  ngpocelbl  25023  bl2ioo  25111  xrtgioo  25126  om1elbas  25353  elpi1  25366  isclm  25385  isclmp  25418  isncvsngp  25470  iscph  25491  tcphcph  25558  lmmbr2  25580  lmmbrf  25583  iscau2  25598  caussi  25618  lmclim  25624  bcthlem1  25645  srabn  25681  ishl2  25691  evthicc2  25781  ovolfioo  25788  ovolficc  25789  iblcnlem1  26108  iblrelem  26111  iblre  26114  iblcn  26119  isuc1p  26459  ismon1p  26461  ellogrn  26887  logreclem  27090  atandm  27204  atandm2  27205  atandm3  27206  atans2  27259  dmarea  27285  dchrelbas4  27570  lgsmodeq  27669  lgsmulsqcoprm  27670  flt4lem5e  27986  nocvxminlem  28140  cutcuts  28167  cutbday  28170  addcuts2  28365  mulcut2  28519  ax5seg  29516  eengtrkg  29564  uspgredg2v  29805  nb3grpr2  29964  isrusgr0  30147  rusgrprop0  30148  ewlkprop  30184  wksfval  30190  wlkeq  30214  wlkson  30235  wlkonprop  30237  upgr2wlk  30247  upgrtrls  30284  upgristrl  30285  wksonproplem  30287  pthsfval  30304  ispth  30306  dfpth2  30314  isspthonpth  30335  uhgrwkspth  30341  usgr2wlkspth  30345  crctcshwlkn0lem4  30402  wspthnp  30439  wwlknon  30446  wwlksnextwrd  30486  wwlksnextinj  30488  wspthsnwspthsnon  30505  umgr2adedgwlk  30534  umgr2adedgwlkon  30535  umgr2adedgwlkonALT  30536  umgr2adedgspth  30537  s3wwlks2on  30545  sps3wwlks2on  30546  wpthswwlks2on  30553  usgr2wspthons3  30556  usgr2wspthon  30557  elwwlks2  30558  elwspths2spth  30559  rusgrnumwwlkl1  30560  rusgrnumwwlkslem  30561  isclwwlk  30575  clwwlkbp  30576  clwlkclwwlklem3  30592  isclwwlknx  30627  clwwlknp  30628  clwwlkn1  30632  clwwlkn2  30635  clwwlkwwlksb  30645  clwwlknonel  30686  0pth  30716  frcond4  30871  1to3vfriswmgr  30881  3cyclfrgr  30889  frgrwopreglem5  30922  2clwwlk2clwwlk  30951  numclwlk1lem1  30970  numclwwlk6  30991  ajval  31463  issh  31810  dmadjss  32489  adjeu  32491  adjval  32492  isst  32815  ishst  32816  xrdifh  33372  nndiffz1  33378  xdivpnfrp  33499  isslmd  33763  ismxidl  33987  ressply1mon1p  34100  isrrext  34632  ismntop  34658  isros  34801  issros  34808  issibf  34965  eulerpartleme  34995  eulerpartlemt0  35001  probun  35051  bnj250  35332  bnj255  35336  bnj345  35345  bnj945  35404  bnj1209  35426  bnj1275  35443  bnj543  35523  bnj571  35536  bnj607  35546  bnj882  35556  bnj983  35581  bnj996  35586  bnj1006  35590  bnj1033  35599  bnj1097  35611  bnj1110  35612  bnj1145  35623  bnj1174  35633  bnj1189  35639  bnj1450  35680  bnj1514  35693  axprALT2  35734  wevgblacfn  35890  cusgr3cyclex  35911  erdszelem1  35956  cvmsval  36031  cvmliftiota  36066  snmlval  36096  lediv2aALT  36442  elwlim  36585  brtxp2  36643  brpprod3a  36648  brcart  36694  lemsuccf  36703  broutsideof3  36891  ivthALT  37123  df3nandALT2  37188  andnand1  37189  topdifinffinlem  38271  relowlssretop  38287  rdgeqoa  38294  unccur  38527  fin2solem  38530  poimirlem3  38542  poimirlem4  38543  poimirlem26  38565  poimirlem27  38566  poimirlem32  38571  itg2gt0cn  38594  iblabsnclem  38602  areacirc  38632  impprop  38645  neificl  38688  ablo4pnp  38815  isrngohom  38900  isidl  38949  ispridl  38969  pridlidl  38970  ismaxidl  38975  maxidlidl  38976  isfldidl2  39004  isdmn3  39009  triantru3  39169  moantr  39305  brxrn2  39317  dfxrn2  39318  ecxrn  39339  disjressuc2  39344  inxpxrn  39351  rnxrn  39354  dfsuccl4  39407  dmqsblocks  39900  islshp  40037  isopos  40238  cvrfval  40326  cvrval  40327  isatl  40357  isat3  40365  islpln5  40593  4atlem11  40667  dalem20  40751  lhpexle3  41070  lhpex2leN  41071  isltrn2N  41178  diclspsn  42252  lcfls1lem  42592  lcfls1N  42593  uzindd  43029  isprimroot  43144  3cubes  43701  fz1eqin  43780  dflim6  44266  dflim7  44275  nnoeomeqom  44314  cantnfub2  44324  fzunt  44456  fzuntd  44457  fzunt1d  44458  fzuntgd  44459  rp-isfinite6  44519  snhesn  44786  ismnuprim  45278  ismnushort  45285  iotasbc2  45404  eelT00  45687  eelTTT  45688  eelT11  45689  eelT12  45691  eelTT1  45692  eelT01  45693  eel0T1  45694  uun132  45767  uun132p1  45768  un2122  45772  uunTT1  45775  uunTT1p1  45776  uunTT1p2  45777  uunT11  45778  uunT11p1  45779  uunT11p2  45780  uunT12  45781  uunT12p1  45782  uunT12p2  45783  uunT12p3  45784  uunT12p4  45785  uunT12p5  45786  uun111  45787  uun2221  45795  uun2221p1  45796  uun2221p2  45797  stoweidlem17  47027  stoweidlem34  47044  stoweidlem60  47070  ndmaovass  48276  ndmaovdistr  48277  4an21  48340  2elfz3nn0  48386  difltmodne  48418  prproropf1o  48589  fpprel  48826  clnbgredg  48938  dfvopnbgr2  48951  dfclnbgr6  48954  dfnbgr6  48955  dfsclnbgr6  48956  uhgrimprop  48990  isuspgrimlem  48993  clnbgrgrim  49032  isgrtri  49041  isubgr3stgrlem4  49067  isubgr3stgrlem7  49070  upwlksfval  49233  isupwlkg  49235  upwlkbprop  49236  2zrngnmrid  49353  isidom3  49442  lindslinindsimp2lem5  49574  i0oii  50028  io1ii  50029  sepnsepolem1  50030  isthincd2  50545  functhinc  50556  elpg  50807  alimp-no-surprise  50877