Theorem 3anass 1101

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

Syntax hints:   ↔ wb 208   ∧ wa 397   ∧ w3a 1093

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 398  df-3an 1095

This theorem is referenced by:  3anan12  1102  3ancoma  1104  anandi3  1108  4anpull2  1369  3biant1d  1487  an33rean  1492  cad1  1625  3exdistr  1968  ceqsex2  3484  ceqsex2v  3485  ceqsex3v  3486  ceqsex4v  3487  ceqsex6v  3488  ceqsex8v  3489  2reu5lem1  3698  2reu5lem2  3699  2reu5lem3  3700  eldifpr  4593  rexdifpr  4594  trel3  5191  2rbropap  5509  ordelord  6336  dflim2  6372  dff1o4  6779  foco2  7054  brfvopab  7417  eloprabga  7469  ndmovass  7548  ndmovdistr  7549  dflim3  7791  dflim4  7792  frxp2  8088  mpoxopovel  8164  dfsmo2  8281  dfrecs3  8306  oeeui  8532  naddasslem2  8625  ecopovtrn  8761  elixp2  8843  elixp  8846  mptelixpg  8877  dif1en  9090  ssfi  9101  sbthfilem  9126  eqinf  9392  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  20523  issubrg3  20576  isdomn3  20691  issdrg  20764  sdrgacs  20777  islmod  20858  lsspropd  21011  islmhm  21021  islbs  21070  lbspropd  21093  qusmulrng  21279  rngqiprngghmlem3  21286  rngqiprnglinlem3  21290  rngqiprnglin  21299  cnfldfunALT  21366  isphl  21607  elocv  21647  isobs  21699  mat1dimscm  22462  scmatghm  22520  scmatmhm  22521  ma1repvcl  22557  smadiadetr  22662  mat2pmatghm  22717  mat2pmatmul  22718  decpmatmulsumfsupp  22760  pm2mpghm  22803  pm2mpmhmlem1  22805  neindisj  23104  lmbrf  23247  hauscmplem  23393  llyi  23461  subislly  23468  islocfin  23504  uptx  23612  txcn  23613  qtopeu  23703  elmptrab  23814  isfbas  23816  trfil2  23874  flimcls  23972  cnextcn  24054  xmetec  24421  ngppropd  24624  ngpocelbl  24691  bl2ioo  24779  xrtgioo  24794  om1elbas  25021  elpi1  25034  isclm  25053  isclmp  25086  isncvsngp  25138  iscph  25159  tcphcph  25226  lmmbr2  25248  lmmbrf  25251  iscau2  25266  caussi  25286  lmclim  25292  bcthlem1  25313  srabn  25349  ishl2  25359  evthicc2  25449  ovolfioo  25456  ovolficc  25457  iblcnlem1  25777  iblrelem  25780  iblre  25783  iblcn  25788  isuc1p  26128  ismon1p  26130  ellogrn  26545  logreclem  26748  atandm  26862  atandm2  26863  atandm3  26864  atans2  26917  dmarea  26943  dchrelbas4  27228  lgsmodeq  27327  lgsmulsqcoprm  27328  nocvxminlem  27768  cutcuts  27795  cutbday  27798  addcuts2  27993  mulcut2  28147  ax5seg  29029  eengtrkg  29077  uspgredg2v  29315  nb3grpr2  29474  isrusgr0  29657  rusgrprop0  29658  ewlkprop  29694  wksfval  29700  wlkeq  29724  wlkson  29745  wlkonprop  29747  upgr2wlk  29757  upgrtrls  29790  upgristrl  29791  wksonproplem  29793  pthsfval  29809  ispth  29811  dfpth2  29819  isspthonpth  29839  uhgrwkspth  29845  usgr2wlkspth  29849  crctcshwlkn0lem4  29903  wspthnp  29940  wwlknon  29947  wwlksnextwrd  29987  wwlksnextinj  29989  wspthsnwspthsnon  30006  umgr2adedgwlk  30035  umgr2adedgwlkon  30036  umgr2adedgwlkonALT  30037  umgr2adedgspth  30038  s3wwlks2on  30046  sps3wwlks2on  30047  wpthswwlks2on  30054  usgr2wspthons3  30057  usgr2wspthon  30058  elwwlks2  30059  elwspths2spth  30060  rusgrnumwwlkl1  30061  rusgrnumwwlkslem  30062  isclwwlk  30076  clwwlkbp  30077  clwlkclwwlklem3  30093  isclwwlknx  30128  clwwlknp  30129  clwwlkn1  30133  clwwlkn2  30136  clwwlkwwlksb  30146  clwwlknonel  30187  0pth  30217  frcond4  30362  1to3vfriswmgr  30372  3cyclfrgr  30380  frgrwopreglem5  30413  2clwwlk2clwwlk  30442  numclwlk1lem1  30461  numclwwlk6  30482  ajval  30954  issh  31301  dmadjss  31980  adjeu  31982  adjval  31983  isst  32306  ishst  32307  xrdifh  32876  nndiffz1  32882  xdivpnfrp  33015  isslmd  33287  isprmidl  33525  isprmidlc  33534  ismxidl  33549  ressply1mon1p  33663  isrrext  34196  ismntop  34222  isros  34364  issros  34371  issibf  34529  eulerpartleme  34559  eulerpartlemt0  34565  probun  34615  bnj250  34899  bnj255  34903  bnj345  34912  bnj945  34971  bnj1209  34993  bnj1275  35010  bnj543  35090  bnj571  35103  bnj607  35113  bnj882  35123  bnj983  35148  bnj996  35153  bnj1006  35157  bnj1033  35166  bnj1097  35178  bnj1110  35179  bnj1145  35190  bnj1174  35200  bnj1189  35206  bnj1450  35247  bnj1514  35260  axprALT2  35305  wevgblacfn  35352  cusgr3cyclex  35379  erdszelem1  35434  cvmsval  35509  cvmliftiota  35544  snmlval  35574  lediv2aALT  35920  elwlim  36064  brtxp2  36122  brpprod3a  36127  brcart  36173  lemsuccf  36182  broutsideof3  36369  ivthALT  36578  df3nandALT2  36643  andnand1  36644  topdifinffinlem  37724  relowlssretop  37740  rdgeqoa  37747  unccur  37985  fin2solem  37988  poimirlem3  38005  poimirlem4  38006  poimirlem26  38028  poimirlem27  38029  poimirlem32  38034  itg2gt0cn  38057  iblabsnclem  38065  areacirc  38095  neificl  38135  ablo4pnp  38262  isrngohom  38347  isidl  38396  ispridl  38416  pridlidl  38417  ismaxidl  38422  maxidlidl  38423  isfldidl2  38451  isdmn3  38456  triantru3  38618  moantr  38754  brxrn2  38766  dfxrn2  38767  ecxrn  38788  disjressuc2  38793  inxpxrn  38800  rnxrn  38803  dfsuccl4  38856  dmqsblocks  39349  islshp  39486  isopos  39687  cvrfval  39775  cvrval  39776  isatl  39806  isat3  39814  islpln5  40042  4atlem11  40116  dalem20  40200  lhpexle3  40519  lhpex2leN  40520  isltrn2N  40627  diclspsn  41701  lcfls1lem  42041  lcfls1N  42042  uzindd  42478  isprimroot  42593  flt4lem5e  43121  3cubes  43154  fz1eqin  43233  dflim6  43724  dflim7  43733  nnoeomeqom  43772  cantnfub2  43782  fzunt  43914  fzuntd  43915  fzunt1d  43916  fzuntgd  43917  rp-isfinite6  43977  snhesn  44245  ismnuprim  44753  ismnushort  44760  iotasbc2  44879  eelT00  45163  eelTTT  45164  eelT11  45165  eelT12  45167  eelTT1  45168  eelT01  45169  eel0T1  45170  uun132  45243  uun132p1  45244  un2122  45248  uunTT1  45251  uunTT1p1  45252  uunTT1p2  45253  uunT11  45254  uunT11p1  45255  uunT11p2  45256  uunT12  45257  uunT12p1  45258  uunT12p2  45259  uunT12p3  45260  uunT12p4  45261  uunT12p5  45262  uun111  45263  uun2221  45271  uun2221p1  45272  uun2221p2  45273  stoweidlem17  46474  stoweidlem34  46491  stoweidlem60  46517  ndmaovass  47683  ndmaovdistr  47684  4an21  47747  2elfz3nn0  47793  difltmodne  47825  prproropf1o  47996  fpprel  48233  clnbgredg  48345  dfvopnbgr2  48358  dfclnbgr6  48361  dfnbgr6  48362  dfsclnbgr6  48363  uhgrimprop  48397  isuspgrimlem  48400  clnbgrgrim  48439  isgrtri  48448  isubgr3stgrlem4  48474  isubgr3stgrlem7  48477  upwlksfval  48640  isupwlkg  48642  upwlkbprop  48643  2zrngnmrid  48761  lindslinindsimp2lem5  48967  i0oii  49424  io1ii  49425  sepnsepolem1  49426  isthincd2  49941  functhinc  49952  elpg  50218  alimp-no-surprise  50285