Theorem 3anass 1095

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

Syntax hints:   ↔ wb 205   ∧ wa 397   ∧ w3a 1087

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

This theorem is referenced by:  3anan12  1096  3ancoma  1098  anandi3  1102  3biant1d  1478  an33rean  1483  an33reanOLD  1484  cad1  1618  3exdistr  1964  ceqsex2  3496  ceqsex2v  3497  ceqsex3v  3498  ceqsex4v  3499  ceqsex6v  3500  ceqsex8v  3501  2reu5lem1  3708  2reu5lem2  3709  2reu5lem3  3710  eldifpr  4613  rexdifpr  4614  trel3  5227  2rbropap  5517  ordelord  6332  dflim2  6367  dff1o4  6784  foco2  7048  brfvopab  7403  eloprabga  7453  ndmovass  7531  ndmovdistr  7532  dflim3  7770  dflim4  7771  mpoxopovel  8115  dfsmo2  8257  dfrecs3  8282  dfrecs3OLD  8283  oeeui  8513  ecopovtrn  8689  elixp2  8769  elixp  8772  mptelixpg  8803  dif1en  9034  dif1enOLD  9036  ssfi  9047  sbthfilem  9075  eqinf  9350  zorn2lem7  10368  grothprim  10700  grothtsk  10701  divmulasscom  11767  muldivdir  11778  divmuldiv  11785  sup3  12042  dfnn3  12097  prime  12511  eluz2  12698  raluz2  12747  elixx1  13198  elixx3g  13202  elioo2  13230  elioo5  13246  elicc4  13256  iccneg  13314  icoshft  13315  difreicc  13326  elfz1  13354  elfz  13355  elfz2  13356  elfzm11  13437  elfz2nn0  13457  elfzo2  13500  elfzo3  13514  lbfzo0  13537  fzind2  13615  zmodid2  13729  hashgt23el  14248  swrdnd2  14471  swrdnd0  14473  swrdccatin1  14541  swrdccat  14551  repswswrd  14600  swrdco  14654  2swrd2eqwrdeq  14770  ccat2s1fvwALTOLD  14774  rediv  14946  imdiv  14953  cosmul  15986  bitsval  16235  bitsmod  16247  bitscmp  16249  smueqlem  16301  dfgcd2  16358  lcmneg  16410  lcmftp  16443  coprmgcdb  16456  divgcdcoprmex  16473  cncongr1  16474  cncongr2  16475  difsqpwdvds  16690  oddprmdvds  16706  elgz  16734  xpsfrnel  17375  xpsfrnel2  17377  ismre  17401  mreexexlem4d  17458  iscatd2  17492  isssc  17634  eldmcoa  17882  isdrs  18121  isipodrs  18357  mgmsscl  18433  ismhm  18534  mhmpropd  18538  issubm  18544  issubmndb  18546  submacs  18567  issubg  18856  eqglact  18908  eqgid  18909  pgrpsubgsymgbi  19117  isslw  19314  efgsdm  19436  mulgmhm  19529  mulgghm  19530  dmdprd  19700  dprdw  19712  subgdmdprd  19736  dmdprdpr  19751  issrg  19842  srglmhm  19870  srgrmhm  19871  isring  19886  ringlghm  19942  dfrhm2  20060  issubrg3  20161  issdrg  20172  sdrgacs  20179  islmod  20237  lsspropd  20389  islmhm  20399  islbs  20448  lbspropd  20471  cnfldfunALT  20720  isphl  20943  elocv  20983  isobs  21037  mat1dimscm  21734  scmatghm  21792  scmatmhm  21793  ma1repvcl  21829  smadiadetr  21934  mat2pmatghm  21989  mat2pmatmul  21990  decpmatmulsumfsupp  22032  pm2mpghm  22075  pm2mpmhmlem1  22077  neindisj  22378  lmbrf  22521  hauscmplem  22667  llyi  22735  subislly  22742  islocfin  22778  uptx  22886  txcn  22887  qtopeu  22977  elmptrab  23088  isfbas  23090  trfil2  23148  flimcls  23246  cnextcn  23328  xmetec  23697  ngppropd  23903  ngpocelbl  23978  bl2ioo  24065  xrtgioo  24079  om1elbas  24305  elpi1  24318  isclm  24337  isclmp  24370  isncvsngp  24423  iscph  24444  tcphcph  24511  lmmbr2  24533  lmmbrf  24536  iscau2  24551  caussi  24571  lmclim  24577  bcthlem1  24598  srabn  24634  ishl2  24644  evthicc2  24734  ovolfioo  24741  ovolficc  24742  iblcnlem1  25062  iblrelem  25065  iblre  25068  iblcn  25073  isuc1p  25415  ismon1p  25417  ellogrn  25825  logreclem  26022  atandm  26136  atandm2  26137  atandm3  26138  atans2  26191  dmarea  26217  dchrelbas4  26501  lgsmodeq  26600  lgsmulsqcoprm  26601  nocvxminlem  27027  scutcut  27050  scutbday  27053  ax5seg  27661  eengtrkg  27709  uspgredg2v  27946  nb3grpr2  28105  isrusgr0  28288  rusgrprop0  28289  ewlkprop  28325  wksfval  28331  wlkeq  28356  wlkson  28378  wlkonprop  28380  upgr2wlk  28390  upgrtrls  28423  upgristrl  28424  wksonproplem  28426  wksonproplemOLD  28427  pthsfval  28443  ispth  28445  isspthonpth  28471  uhgrwkspth  28477  usgr2wlkspth  28481  crctcshwlkn0lem4  28532  wspthnp  28569  wwlknon  28576  wwlksnextwrd  28616  wwlksnextinj  28618  wspthsnwspthsnon  28635  umgr2adedgwlk  28664  umgr2adedgwlkon  28665  umgr2adedgwlkonALT  28666  umgr2adedgspth  28667  s3wwlks2on  28675  wpthswwlks2on  28680  usgr2wspthons3  28683  usgr2wspthon  28684  elwwlks2  28685  elwspths2spth  28686  rusgrnumwwlkl1  28687  rusgrnumwwlkslem  28688  isclwwlk  28702  clwwlkbp  28703  clwlkclwwlklem3  28719  isclwwlknx  28754  clwwlknp  28755  clwwlkn1  28759  clwwlkn2  28762  clwwlkwwlksb  28772  clwwlknonel  28813  0pth  28843  frcond4  28988  1to3vfriswmgr  28998  3cyclfrgr  29006  frgrwopreglem5  29039  2clwwlk2clwwlk  29068  numclwlk1lem1  29087  numclwwlk6  29108  ajval  29577  issh  29924  dmadjss  30603  adjeu  30605  adjval  30606  isst  30929  ishst  30930  xrdifh  31452  nndiffz1  31458  xdivpnfrp  31558  isomnd  31678  isslmd  31806  isprmidl  31974  isprmidlc  31984  ismxidl  31995  isrrext  32312  ismntop  32338  isros  32498  issros  32505  issibf  32664  eulerpartleme  32694  eulerpartlemt0  32700  probun  32750  bnj250  33044  bnj255  33048  bnj345  33057  bnj945  33116  bnj1209  33139  bnj1275  33156  bnj543  33236  bnj571  33249  bnj607  33259  bnj882  33269  bnj983  33294  bnj996  33299  bnj1006  33303  bnj1033  33312  bnj1097  33324  bnj1110  33325  bnj1145  33336  bnj1174  33346  bnj1189  33352  bnj1450  33393  bnj1514  33406  cusgr3cyclex  33461  erdszelem1  33516  cvmsval  33591  cvmliftiota  33626  snmlval  33656  lediv2aALT  33998  frxp2  34137  elwlim  34160  naddasslem2  34195  brtxp2  34322  brpprod3a  34327  brcart  34373  brsuccf  34382  broutsideof3  34567  ivthALT  34663  df3nandALT2  34728  andnand1  34729  topdifinffinlem  35674  relowlssretop  35690  rdgeqoa  35697  unccur  35916  fin2solem  35919  poimirlem3  35936  poimirlem4  35937  poimirlem26  35959  poimirlem27  35960  poimirlem32  35965  itg2gt0cn  35988  iblabsnclem  35996  areacirc  36026  neificl  36067  ablo4pnp  36194  isrngohom  36279  isidl  36328  ispridl  36348  pridlidl  36349  ismaxidl  36354  maxidlidl  36355  isfldidl2  36383  isdmn3  36388  triantru3  36541  moantr  36681  brxrn2  36693  dfxrn2  36694  ecxrn  36705  disjressuc2  36706  inxpxrn  36713  rnxrn  36716  islshp  37297  isopos  37498  cvrfval  37586  cvrval  37587  isatl  37617  isat3  37625  islpln5  37854  4atlem11  37928  dalem20  38012  lhpexle3  38331  lhpex2leN  38332  isltrn2N  38439  diclspsn  39513  lcfls1lem  39853  lcfls1N  39854  uzindd  40290  flt4lem5e  40806  3cubes  40825  fz1eqin  40904  isdomn3  41343  fzunt  41436  fzuntd  41437  fzunt1d  41438  fzuntgd  41439  rp-isfinite6  41499  snhesn  41767  ismnuprim  42285  ismnushort  42292  iotasbc2  42411  eelT00  42698  eelTTT  42699  eelT11  42700  eelT12  42702  eelTT1  42703  eelT01  42704  eel0T1  42705  uun132  42778  uun132p1  42779  un2122  42783  uunTT1  42786  uunTT1p1  42787  uunTT1p2  42788  uunT11  42789  uunT11p1  42790  uunT11p2  42791  uunT12  42792  uunT12p1  42793  uunT12p2  42794  uunT12p3  42795  uunT12p4  42796  uunT12p5  42797  uun111  42798  uun2221  42806  uun2221p1  42807  uun2221p2  42808  stoweidlem17  43946  stoweidlem34  43963  stoweidlem60  43989  ndmaovass  45116  ndmaovdistr  45117  4an21  45180  2elfz3nn0  45226  prproropf1o  45377  fpprel  45598  upwlksfval  45715  isupwlkg  45717  upwlkbprop  45718  isrng  45852  2zrngnmrid  45926  lindslinindsimp2lem5  46221  i0oii  46630  io1ii  46631  sepnsepolem1  46632  iscnrm3lem3  46646  isthincd2  46736  functhinc  46743  elpg  46836  alimp-no-surprise  46902