Theorem 3anass 1088

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 1082	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		anass 469	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3	1, 2	bitri 276	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

Syntax hints:   ↔ wb 207   ∧ wa 396   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  3anan12  1089  3ancoma  1091  anandi3  1095  3biant1d  1470  an33rean  1475  cad1  1602  3exdistr  1943  ceqsex2  3489  ceqsex2v  3490  ceqsex3v  3491  ceqsex4v  3492  ceqsex6v  3493  ceqsex8v  3494  2reu5lem1  3685  2reu5lem2  3686  2reu5lem3  3687  eldifpr  4508  rexdifpr  4509  trel3  5078  2rbropap  5346  ordelord  6095  dflim2  6129  dff1o4  6498  foco2  6743  brfvopab  7077  ndmovass  7199  ndmovdistr  7200  dflim3  7425  dflim4  7426  mpoxopovel  7744  dfsmo2  7843  dfrecs3  7868  oeeui  8085  ecopovtrn  8257  elixp2  8321  elixp  8324  mptelixpg  8354  eqinf  8801  zorn2lem7  9777  grothprim  10109  grothtsk  10110  divmulasscom  11176  muldivdir  11187  divmuldiv  11194  sup3  11452  dfnn3  11506  prime  11917  eluz2  12103  raluz2  12150  elixx1  12601  elixx3g  12605  elioo2  12633  elioo5  12648  elicc4  12657  iccneg  12712  icoshft  12713  difreicc  12724  elfz1  12751  elfz  12752  elfz2  12753  elfzm11  12832  elfz2nn0  12852  elfzo2  12895  elfzo3  12908  lbfzo0  12931  fzind2  13009  zmodid2  13121  hashgt23el  13637  swrdnd2  13857  swrdnd0  13859  swrdccatin1  13927  swrdccat  13937  repswswrd  13986  swrdco  14039  2swrd2eqwrdeq  14155  ccat2s1fvwALT  14157  rediv  14328  imdiv  14335  cosmul  15363  bitsval  15610  bitsmod  15622  bitscmp  15624  smueqlem  15676  dfgcd2  15727  lcmneg  15780  lcmftp  15813  coprmgcdb  15826  divgcdcoprmex  15843  cncongr1  15844  cncongr2  15845  difsqpwdvds  16056  oddprmdvds  16072  elgz  16100  xpsfrnel  16668  xpsfrnel2  16670  ismre  16694  mreexexlem4d  16751  iscatd2  16785  isssc  16923  eldmcoa  17158  isdrs  17377  isipodrs  17604  ismhm  17780  mhmpropd  17784  issubm  17790  submacs  17808  issubg  18037  eqglact  18088  eqgid  18089  pgrpsubgsymgbi  18270  isslw  18467  efgsdm  18587  mulgmhm  18677  mulgghm  18678  dmdprd  18841  dprdw  18853  subgdmdprd  18877  dmdprdpr  18892  issrg  18951  srglmhm  18979  srgrmhm  18980  isring  18995  ringlghm  19048  dfrhm2  19163  issubrg3  19257  issdrg  19268  sdrgacs  19274  islmod  19332  lsspropd  19483  islmhm  19493  islbs  19542  lbspropd  19565  isphl  20458  elocv  20498  isobs  20550  mat1dimscm  20772  scmatghm  20830  scmatmhm  20831  ma1repvcl  20867  smadiadetr  20972  mat2pmatghm  21026  mat2pmatmul  21027  decpmatmulsumfsupp  21069  pm2mpghm  21112  pm2mpmhmlem1  21114  neindisj  21413  lmbrf  21556  hauscmplem  21702  llyi  21770  subislly  21777  islocfin  21813  uptx  21921  txcn  21922  qtopeu  22012  elmptrab  22123  isfbas  22125  trfil2  22183  flimcls  22281  cnextcn  22363  xmetec  22731  ngppropd  22933  ngpocelbl  23000  bl2ioo  23087  xrtgioo  23101  om1elbas  23323  elpi1  23336  isclm  23355  isclmp  23388  isncvsngp  23440  iscph  23461  tcphcph  23527  lmmbr2  23549  lmmbrf  23552  iscau2  23567  caussi  23587  lmclim  23593  bcthlem1  23614  srabn  23650  ishl2  23660  evthicc2  23748  ovolfioo  23755  ovolficc  23756  iblcnlem1  24075  iblrelem  24078  iblre  24081  iblcn  24086  isuc1p  24421  ismon1p  24423  ellogrn  24828  logreclem  25025  atandm  25139  atandm2  25140  atandm3  25141  atans2  25194  dmarea  25221  dchrelbas4  25505  lgsmodeq  25604  lgsmulsqcoprm  25605  ax5seg  26411  eengtrkg  26459  uspgredg2v  26693  nb3grpr2  26852  isrusgr0  27035  rusgrprop0  27036  ewlkprop  27072  wksfval  27078  wlkeq  27102  wlkson  27124  wlkonprop  27126  upgr2wlk  27136  upgrtrls  27169  upgristrl  27170  wksonproplem  27172  pthsfval  27188  ispth  27190  isspthonpth  27216  uhgrwkspth  27222  usgr2wlkspth  27226  crctcshwlkn0lem4  27277  wspthnp  27314  wwlknon  27321  wwlksnextwrd  27361  wwlksnextinj  27363  wspthsnwspthsnon  27381  umgr2adedgwlk  27410  umgr2adedgwlkon  27411  umgr2adedgwlkonALT  27412  umgr2adedgspth  27413  s3wwlks2on  27421  wpthswwlks2on  27426  usgr2wspthons3  27429  usgr2wspthon  27430  elwwlks2  27431  elwspths2spth  27432  rusgrnumwwlkl1  27433  rusgrnumwwlkslem  27434  isclwwlk  27448  clwwlkbp  27449  clwlkclwwlklem3  27465  isclwwlknx  27500  clwwlknp  27501  clwwlkn1  27505  clwwlkn2  27508  clwwlkwwlksb  27519  clwwlknonel  27560  0pth  27590  frcond4  27737  1to3vfriswmgr  27747  3cyclfrgr  27755  frgrwopreglem5  27788  2clwwlk2clwwlk  27817  numclwlk1lem1  27836  numclwwlk6  27857  ajval  28325  issh  28672  dmadjss  29351  adjeu  29353  adjval  29354  isst  29677  ishst  29678  xrdifh  30187  nndiffz1  30193  xdivpnfrp  30289  isomnd  30358  isslmd  30464  isrrext  30854  ismntop  30880  isros  31040  issros  31047  issibf  31204  eulerpartleme  31234  eulerpartlemt0  31240  probun  31290  bnj250  31584  bnj255  31588  bnj345  31597  bnj945  31658  bnj1209  31681  bnj1275  31698  bnj543  31777  bnj571  31790  bnj607  31800  bnj882  31810  bnj983  31835  bnj996  31839  bnj1006  31843  bnj1033  31851  bnj1097  31863  bnj1110  31864  bnj1145  31875  bnj1174  31885  bnj1189  31891  bnj1450  31932  bnj1514  31945  cusgr3cyclex  31993  erdszelem1  32048  cvmsval  32123  cvmliftiota  32158  snmlval  32188  lediv2aALT  32530  elwlim  32721  nocvxminlem  32858  scutcut  32877  scutbday  32878  brtxp2  32953  brpprod3a  32958  brcart  33004  brsuccf  33013  broutsideof3  33198  ivthALT  33294  df3nandALT2  33359  andnand1  33360  topdifinffinlem  34180  relowlssretop  34196  rdgeqoa  34203  unccur  34427  fin2solem  34430  poimirlem3  34447  poimirlem4  34448  poimirlem26  34470  poimirlem27  34471  poimirlem32  34476  itg2gt0cn  34499  iblabsnclem  34507  areacirc  34539  neificl  34581  ablo4pnp  34711  isrngohom  34796  isidl  34845  ispridl  34865  pridlidl  34866  ismaxidl  34871  maxidlidl  34872  isfldidl2  34900  isdmn3  34905  triantru3  35053  moantr  35169  brxrn2  35179  dfxrn2  35180  ecxrn  35191  inxpxrn  35195  rnxrn  35198  islshp  35667  isopos  35868  cvrfval  35956  cvrval  35957  isatl  35987  isat3  35995  islpln5  36223  4atlem11  36297  dalem20  36381  lhpexle3  36700  lhpex2leN  36701  isltrn2N  36808  diclspsn  37882  lcfls1lem  38222  lcfls1N  38223  fz1eqin  38872  isdomn3  39310  rp-isfinite6  39390  snhesn  39638  ismnuprim  40148  iotasbc2  40311  eelT00  40599  eelTTT  40600  eelT11  40601  eelT12  40603  eelTT1  40604  eelT01  40605  eel0T1  40606  uun132  40679  uun132p1  40680  un2122  40684  uunTT1  40687  uunTT1p1  40688  uunTT1p2  40689  uunT11  40690  uunT11p1  40691  uunT11p2  40692  uunT12  40693  uunT12p1  40694  uunT12p2  40695  uunT12p3  40696  uunT12p4  40697  uunT12p5  40698  uun111  40699  uun2221  40707  uun2221p1  40708  uun2221p2  40709  stoweidlem17  41866  stoweidlem34  41883  stoweidlem60  41909  ndmaovass  42943  ndmaovdistr  42944  4an21  43007  2elfz3nn0  43054  prproropf1o  43173  fpprel  43397  upwlksfval  43514  isupwlkg  43516  upwlkbprop  43517  isrng  43647  2zrngnmrid  43721  lindslinindsimp2lem5  44019  elpg  44318  alimp-no-surprise  44384