Theorem 3anass 1107

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

Syntax hints:   ↔ wb 208   ∧ wa 399   ∧ w3a 1099

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 209  df-an 400  df-3an 1101

This theorem is referenced by:  3anan12  1108  3ancoma  1111  anandi3  1115  4anpull2OLD  1377  3biant1d  1501  an33rean  1506  cad1  1639  3exdistr  1982  ceqsex2  3506  ceqsex2v  3507  ceqsex3v  3508  ceqsex4v  3509  ceqsex6v  3510  ceqsex8v  3511  2reu5lem1  3720  2reu5lem2  3721  2reu5lem3  3722  eldifpr  4619  rexdifpr  4620  trel3  5218  2rbropap  5537  ordelord  6370  dflim2  6406  dff1o4  6817  foco2  7092  brfvopab  7455  eloprabga  7507  ndmovass  7586  ndmovdistr  7587  dflim3  7829  dflim4  7830  frxp2  8126  mpoxopovel  8202  dfsmo2  8320  dfrecs3  8345  oeeui  8574  naddasslem2  8668  ecopovtrn  8804  elixp2  8885  elixp  8888  mptelixpg  8919  dif1en  9132  ssfi  9143  sbthfilem  9168  eqinf  9433  zorn2lem7  10461  grothprim  10794  grothtsk  10795  divmulasscom  11871  muldivdir  11885  divmuldiv  11893  sup3  12151  dfnn3  12226  prime  12656  eluz2  12847  raluz2  12900  elixx1  13360  elixx3g  13364  elioo2  13392  elioo5  13409  elicc4  13419  iccneg  13478  icoshft  13479  difreicc  13490  elfz1  13519  elfz  13520  elfz2  13521  elfzm11  13602  elfz2nn0  13625  elfzo2  13669  elfzo3  13684  lbfzo0  13707  fzo1lb  13721  1elfzo1  13722  fzind2  13796  zmodid2  13911  hashgt23el  14439  swrdnd2  14671  swrdnd0  14673  swrdccatin1  14740  swrdccat  14750  repswswrd  14799  swrdco  14852  2swrd2eqwrdeq  14968  rediv  15160  imdiv  15167  cosmul  16207  bitsval  16460  bitsmod  16472  bitscmp  16474  smueqlem  16526  dfgcd2  16582  lcmneg  16639  lcmftp  16672  coprmgcdb  16685  divgcdcoprmex  16702  cncongr1  16703  cncongr2  16704  difsqpwdvds  16925  oddprmdvds  16941  elgz  16969  xpsfrnel  17594  xpsfrnel2  17596  ismre  17620  mreexexlem4d  17681  iscatd2  17715  isssc  17855  eldmcoa  18100  isdrs  18335  isipodrs  18571  mgmsscl  18681  ismhm  18821  mhmpropd  18828  issubm  18839  issubmndb  18841  submacs  18863  issubg  19170  eqglact  19222  eqgid  19223  ecqusaddd  19235  ecqusaddcl  19236  pgrpsubgsymgbi  19450  isslw  19650  efgsdm  19772  mulgmhm  19869  mulgghm  19870  dmdprd  20042  dprdw  20054  subgdmdprd  20078  dmdprdpr  20093  isomnd  20165  isrng  20202  issrg  20240  srglmhm  20273  srgrmhm  20274  isring  20289  ringlghm  20364  dfrhm2  20525  issubrng  20599  issubrg3  20652  isdomn3  20767  issdrg  20839  sdrgacs  20852  islmod  20933  lsspropd  21086  islmhm  21096  islbs  21145  lbspropd  21168  qusmulrng  21354  rngqiprngghmlem3  21361  rngqiprnglinlem3  21365  rngqiprnglin  21374  cnfldfunALT  21441  isphl  21682  elocv  21722  isobs  21774  mat1dimscm  22537  scmatghm  22595  scmatmhm  22596  ma1repvcl  22632  smadiadetr  22737  mat2pmatghm  22792  mat2pmatmul  22793  decpmatmulsumfsupp  22835  pm2mpghm  22878  pm2mpmhmlem1  22880  neindisj  23179  lmbrf  23322  hauscmplem  23468  llyi  23536  subislly  23543  islocfin  23579  uptx  23687  txcn  23688  qtopeu  23778  elmptrab  23889  isfbas  23891  trfil2  23949  flimcls  24047  cnextcn  24129  xmetec  24496  ngppropd  24699  ngpocelbl  24766  bl2ioo  24854  xrtgioo  24869  om1elbas  25096  elpi1  25109  isclm  25128  isclmp  25161  isncvsngp  25213  iscph  25234  tcphcph  25301  lmmbr2  25323  lmmbrf  25326  iscau2  25341  caussi  25361  lmclim  25367  bcthlem1  25388  srabn  25424  ishl2  25434  evthicc2  25524  ovolfioo  25531  ovolficc  25532  iblcnlem1  25852  iblrelem  25855  iblre  25858  iblcn  25863  isuc1p  26203  ismon1p  26205  ellogrn  26626  logreclem  26829  atandm  26943  atandm2  26944  atandm3  26945  atans2  26998  dmarea  27024  dchrelbas4  27309  lgsmodeq  27408  lgsmulsqcoprm  27409  nocvxminlem  27849  cutcuts  27876  cutbday  27879  addcuts2  28074  mulcut2  28228  ax5seg  29141  eengtrkg  29189  uspgredg2v  29427  nb3grpr2  29586  isrusgr0  29769  rusgrprop0  29770  ewlkprop  29806  wksfval  29812  wlkeq  29836  wlkson  29857  wlkonprop  29859  upgr2wlk  29869  upgrtrls  29902  upgristrl  29903  wksonproplem  29905  pthsfval  29921  ispth  29923  dfpth2  29931  isspthonpth  29951  uhgrwkspth  29957  usgr2wlkspth  29961  crctcshwlkn0lem4  30015  wspthnp  30052  wwlknon  30059  wwlksnextwrd  30099  wwlksnextinj  30101  wspthsnwspthsnon  30118  umgr2adedgwlk  30147  umgr2adedgwlkon  30148  umgr2adedgwlkonALT  30149  umgr2adedgspth  30150  s3wwlks2on  30158  sps3wwlks2on  30159  wpthswwlks2on  30166  usgr2wspthons3  30169  usgr2wspthon  30170  elwwlks2  30171  elwspths2spth  30172  rusgrnumwwlkl1  30173  rusgrnumwwlkslem  30174  isclwwlk  30188  clwwlkbp  30189  clwlkclwwlklem3  30205  isclwwlknx  30240  clwwlknp  30241  clwwlkn1  30245  clwwlkn2  30248  clwwlkwwlksb  30258  clwwlknonel  30299  0pth  30329  frcond4  30474  1to3vfriswmgr  30484  3cyclfrgr  30492  frgrwopreglem5  30525  2clwwlk2clwwlk  30554  numclwlk1lem1  30573  numclwwlk6  30594  ajval  31066  issh  31413  dmadjss  32092  adjeu  32094  adjval  32095  isst  32418  ishst  32419  xrdifh  32984  nndiffz1  32990  xdivpnfrp  33112  isslmd  33384  isprmidl  33626  isprmidlc  33635  ismxidl  33652  ressply1mon1p  33766  isrrext  34299  ismntop  34325  isros  34467  issros  34474  issibf  34632  eulerpartleme  34662  eulerpartlemt0  34668  probun  34718  bnj250  34999  bnj255  35003  bnj345  35012  bnj945  35071  bnj1209  35093  bnj1275  35110  bnj543  35190  bnj571  35203  bnj607  35213  bnj882  35223  bnj983  35248  bnj996  35253  bnj1006  35257  bnj1033  35266  bnj1097  35278  bnj1110  35279  bnj1145  35290  bnj1174  35300  bnj1189  35306  bnj1450  35347  bnj1514  35360  axprALT2  35409  wevgblacfn  35458  cusgr3cyclex  35491  erdszelem1  35546  cvmsval  35621  cvmliftiota  35656  snmlval  35686  lediv2aALT  36032  elwlim  36176  brtxp2  36234  brpprod3a  36239  brcart  36285  lemsuccf  36294  broutsideof3  36481  ivthALT  36700  df3nandALT2  36765  andnand1  36766  topdifinffinlem  37846  relowlssretop  37862  rdgeqoa  37869  unccur  38107  fin2solem  38110  poimirlem3  38127  poimirlem4  38128  poimirlem26  38150  poimirlem27  38151  poimirlem32  38156  itg2gt0cn  38179  iblabsnclem  38187  areacirc  38217  neificl  38257  ablo4pnp  38384  isrngohom  38469  isidl  38518  ispridl  38538  pridlidl  38539  ismaxidl  38544  maxidlidl  38545  isfldidl2  38573  isdmn3  38578  triantru3  38740  moantr  38876  brxrn2  38888  dfxrn2  38889  ecxrn  38910  disjressuc2  38915  inxpxrn  38922  rnxrn  38925  dfsuccl4  38978  dmqsblocks  39471  islshp  39608  isopos  39809  cvrfval  39897  cvrval  39898  isatl  39928  isat3  39936  islpln5  40164  4atlem11  40238  dalem20  40322  lhpexle3  40641  lhpex2leN  40642  isltrn2N  40749  diclspsn  41823  lcfls1lem  42163  lcfls1N  42164  uzindd  42600  isprimroot  42715  flt4lem5e  43243  3cubes  43276  fz1eqin  43355  dflim6  43846  dflim7  43855  nnoeomeqom  43894  cantnfub2  43904  fzunt  44036  fzuntd  44037  fzunt1d  44038  fzuntgd  44039  rp-isfinite6  44099  snhesn  44367  ismnuprim  44875  ismnushort  44882  iotasbc2  45001  eelT00  45285  eelTTT  45286  eelT11  45287  eelT12  45289  eelTT1  45290  eelT01  45291  eel0T1  45292  uun132  45365  uun132p1  45366  un2122  45370  uunTT1  45373  uunTT1p1  45374  uunTT1p2  45375  uunT11  45376  uunT11p1  45377  uunT11p2  45378  uunT12  45379  uunT12p1  45380  uunT12p2  45381  uunT12p3  45382  uunT12p4  45383  uunT12p5  45384  uun111  45385  uun2221  45393  uun2221p1  45394  uun2221p2  45395  stoweidlem17  46596  stoweidlem34  46613  stoweidlem60  46639  ndmaovass  47805  ndmaovdistr  47806  4an21  47869  2elfz3nn0  47915  difltmodne  47947  prproropf1o  48118  fpprel  48355  clnbgredg  48467  dfvopnbgr2  48480  dfclnbgr6  48483  dfnbgr6  48484  dfsclnbgr6  48485  uhgrimprop  48519  isuspgrimlem  48522  clnbgrgrim  48561  isgrtri  48570  isubgr3stgrlem4  48596  isubgr3stgrlem7  48599  upwlksfval  48762  isupwlkg  48764  upwlkbprop  48765  2zrngnmrid  48883  lindslinindsimp2lem5  49089  i0oii  49546  io1ii  49547  sepnsepolem1  49548  isthincd2  50063  functhinc  50074  elpg  50340  alimp-no-surprise  50407