Theorem 3anass 1094

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

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

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 1088

This theorem is referenced by:  3anan12  1095  3ancoma  1097  anandi3  1101  4anpull2  1362  3biant1d  1480  an33rean  1485  cad1  1618  3exdistr  1961  ceqsex2  3489  ceqsex2v  3490  ceqsex3v  3491  ceqsex4v  3492  ceqsex6v  3493  ceqsex8v  3494  2reu5lem1  3709  2reu5lem2  3710  2reu5lem3  3711  eldifpr  4608  rexdifpr  4609  trel3  5205  2rbropap  5502  ordelord  6328  dflim2  6364  dff1o4  6771  foco2  7042  brfvopab  7403  eloprabga  7455  ndmovass  7534  ndmovdistr  7535  dflim3  7777  dflim4  7778  frxp2  8074  mpoxopovel  8150  dfsmo2  8267  dfrecs3  8292  oeeui  8517  naddasslem2  8610  ecopovtrn  8744  elixp2  8825  elixp  8828  mptelixpg  8859  dif1en  9071  ssfi  9082  sbthfilem  9107  eqinf  9369  zorn2lem7  10393  grothprim  10725  grothtsk  10726  divmulasscom  11800  muldivdir  11814  divmuldiv  11821  sup3  12079  dfnn3  12139  prime  12554  eluz2  12738  raluz2  12795  elixx1  13254  elixx3g  13258  elioo2  13286  elioo5  13303  elicc4  13313  iccneg  13372  icoshft  13373  difreicc  13384  elfz1  13412  elfz  13413  elfz2  13414  elfzm11  13495  elfz2nn0  13518  elfzo2  13562  elfzo3  13576  lbfzo0  13599  fzo1lb  13613  1elfzo1  13614  fzind2  13688  zmodid2  13803  hashgt23el  14331  swrdnd2  14563  swrdnd0  14565  swrdccatin1  14632  swrdccat  14642  repswswrd  14691  swrdco  14744  2swrd2eqwrdeq  14860  rediv  15038  imdiv  15045  cosmul  16082  bitsval  16335  bitsmod  16347  bitscmp  16349  smueqlem  16401  dfgcd2  16457  lcmneg  16514  lcmftp  16547  coprmgcdb  16560  divgcdcoprmex  16577  cncongr1  16578  cncongr2  16579  difsqpwdvds  16799  oddprmdvds  16815  elgz  16843  xpsfrnel  17466  xpsfrnel2  17468  ismre  17492  mreexexlem4d  17553  iscatd2  17587  isssc  17727  eldmcoa  17972  isdrs  18207  isipodrs  18443  mgmsscl  18553  ismhm  18693  mhmpropd  18700  issubm  18711  issubmndb  18713  submacs  18735  issubg  19039  eqglact  19091  eqgid  19092  ecqusaddd  19104  ecqusaddcl  19105  pgrpsubgsymgbi  19320  isslw  19520  efgsdm  19642  mulgmhm  19739  mulgghm  19740  dmdprd  19912  dprdw  19924  subgdmdprd  19948  dmdprdpr  19963  isomnd  20035  isrng  20072  issrg  20106  srglmhm  20139  srgrmhm  20140  isring  20155  ringlghm  20230  dfrhm2  20392  issubrng  20462  issubrg3  20515  isdomn3  20630  issdrg  20703  sdrgacs  20716  islmod  20797  lsspropd  20951  islmhm  20961  islbs  21010  lbspropd  21033  qusmulrng  21219  rngqiprngghmlem3  21226  rngqiprnglinlem3  21230  rngqiprnglin  21239  cnfldfunALT  21306  cnfldfunALTOLD  21319  isphl  21565  elocv  21605  isobs  21657  mat1dimscm  22390  scmatghm  22448  scmatmhm  22449  ma1repvcl  22485  smadiadetr  22590  mat2pmatghm  22645  mat2pmatmul  22646  decpmatmulsumfsupp  22688  pm2mpghm  22731  pm2mpmhmlem1  22733  neindisj  23032  lmbrf  23175  hauscmplem  23321  llyi  23389  subislly  23396  islocfin  23432  uptx  23540  txcn  23541  qtopeu  23631  elmptrab  23742  isfbas  23744  trfil2  23802  flimcls  23900  cnextcn  23982  xmetec  24349  ngppropd  24552  ngpocelbl  24619  bl2ioo  24707  xrtgioo  24722  om1elbas  24959  elpi1  24972  isclm  24991  isclmp  25024  isncvsngp  25076  iscph  25097  tcphcph  25164  lmmbr2  25186  lmmbrf  25189  iscau2  25204  caussi  25224  lmclim  25230  bcthlem1  25251  srabn  25287  ishl2  25297  evthicc2  25388  ovolfioo  25395  ovolficc  25396  iblcnlem1  25716  iblrelem  25719  iblre  25722  iblcn  25727  isuc1p  26073  ismon1p  26075  ellogrn  26495  logreclem  26699  atandm  26813  atandm2  26814  atandm3  26815  atans2  26868  dmarea  26894  dchrelbas4  27181  lgsmodeq  27280  lgsmulsqcoprm  27281  nocvxminlem  27717  scutcut  27742  scutbday  27745  addscut2  27922  mulscut2  28072  ax5seg  28916  eengtrkg  28964  uspgredg2v  29202  nb3grpr2  29361  isrusgr0  29545  rusgrprop0  29546  ewlkprop  29582  wksfval  29588  wlkeq  29612  wlkson  29633  wlkonprop  29635  upgr2wlk  29645  upgrtrls  29678  upgristrl  29679  wksonproplem  29681  pthsfval  29697  ispth  29699  dfpth2  29707  isspthonpth  29727  uhgrwkspth  29733  usgr2wlkspth  29737  crctcshwlkn0lem4  29791  wspthnp  29828  wwlknon  29835  wwlksnextwrd  29875  wwlksnextinj  29877  wspthsnwspthsnon  29894  umgr2adedgwlk  29923  umgr2adedgwlkon  29924  umgr2adedgwlkonALT  29925  umgr2adedgspth  29926  s3wwlks2on  29934  sps3wwlks2on  29935  wpthswwlks2on  29942  usgr2wspthons3  29945  usgr2wspthon  29946  elwwlks2  29947  elwspths2spth  29948  rusgrnumwwlkl1  29949  rusgrnumwwlkslem  29950  isclwwlk  29964  clwwlkbp  29965  clwlkclwwlklem3  29981  isclwwlknx  30016  clwwlknp  30017  clwwlkn1  30021  clwwlkn2  30024  clwwlkwwlksb  30034  clwwlknonel  30075  0pth  30105  frcond4  30250  1to3vfriswmgr  30260  3cyclfrgr  30268  frgrwopreglem5  30301  2clwwlk2clwwlk  30330  numclwlk1lem1  30349  numclwwlk6  30370  ajval  30841  issh  31188  dmadjss  31867  adjeu  31869  adjval  31870  isst  32193  ishst  32194  xrdifh  32763  nndiffz1  32769  xdivpnfrp  32913  isslmd  33171  isprmidl  33403  isprmidlc  33412  ismxidl  33427  ressply1mon1p  33531  isrrext  34013  ismntop  34039  isros  34181  issros  34188  issibf  34346  eulerpartleme  34376  eulerpartlemt0  34382  probun  34432  bnj250  34713  bnj255  34717  bnj345  34726  bnj945  34785  bnj1209  34808  bnj1275  34825  bnj543  34905  bnj571  34918  bnj607  34928  bnj882  34938  bnj983  34963  bnj996  34968  bnj1006  34972  bnj1033  34981  bnj1097  34993  bnj1110  34994  bnj1145  35005  bnj1174  35015  bnj1189  35021  bnj1450  35062  bnj1514  35075  wevgblacfn  35153  cusgr3cyclex  35180  erdszelem1  35235  cvmsval  35310  cvmliftiota  35345  snmlval  35375  lediv2aALT  35721  elwlim  35865  brtxp2  35923  brpprod3a  35928  brcart  35974  lemsuccf  35983  broutsideof3  36170  ivthALT  36379  df3nandALT2  36444  andnand1  36445  topdifinffinlem  37391  relowlssretop  37407  rdgeqoa  37414  unccur  37642  fin2solem  37645  poimirlem3  37662  poimirlem4  37663  poimirlem26  37685  poimirlem27  37686  poimirlem32  37691  itg2gt0cn  37714  iblabsnclem  37722  areacirc  37752  neificl  37792  ablo4pnp  37919  isrngohom  38004  isidl  38053  ispridl  38073  pridlidl  38074  ismaxidl  38079  maxidlidl  38080  isfldidl2  38108  isdmn3  38113  triantru3  38270  moantr  38395  brxrn2  38407  dfxrn2  38408  ecxrn  38429  disjressuc2  38434  inxpxrn  38441  rnxrn  38444  dfsuccl4  38486  dmqsblocks  38950  islshp  39077  isopos  39278  cvrfval  39366  cvrval  39367  isatl  39397  isat3  39405  islpln5  39633  4atlem11  39707  dalem20  39791  lhpexle3  40110  lhpex2leN  40111  isltrn2N  40218  diclspsn  41292  lcfls1lem  41632  lcfls1N  41633  uzindd  42069  isprimroot  42185  flt4lem5e  42748  3cubes  42782  fz1eqin  42861  dflim6  43356  dflim7  43365  nnoeomeqom  43404  cantnfub2  43414  fzunt  43547  fzuntd  43548  fzunt1d  43549  fzuntgd  43550  rp-isfinite6  43610  snhesn  43878  ismnuprim  44386  ismnushort  44393  iotasbc2  44512  eelT00  44796  eelTTT  44797  eelT11  44798  eelT12  44800  eelTT1  44801  eelT01  44802  eel0T1  44803  uun132  44876  uun132p1  44877  un2122  44881  uunTT1  44884  uunTT1p1  44885  uunTT1p2  44886  uunT11  44887  uunT11p1  44888  uunT11p2  44889  uunT12  44890  uunT12p1  44891  uunT12p2  44892  uunT12p3  44893  uunT12p4  44894  uunT12p5  44895  uun111  44896  uun2221  44904  uun2221p1  44905  uun2221p2  44906  stoweidlem17  46114  stoweidlem34  46131  stoweidlem60  46157  ndmaovass  47305  ndmaovdistr  47306  4an21  47369  2elfz3nn0  47415  difltmodne  47441  prproropf1o  47606  fpprel  47827  clnbgredg  47939  dfvopnbgr2  47952  dfclnbgr6  47955  dfnbgr6  47956  dfsclnbgr6  47957  uhgrimprop  47991  isuspgrimlem  47994  clnbgrgrim  48033  isgrtri  48042  isubgr3stgrlem4  48068  isubgr3stgrlem7  48071  upwlksfval  48234  isupwlkg  48236  upwlkbprop  48237  2zrngnmrid  48355  lindslinindsimp2lem5  48562  i0oii  49019  io1ii  49020  sepnsepolem1  49021  isthincd2  49537  functhinc  49548  elpg  49814  alimp-no-surprise  49881