Theorem 3anass 1091

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

Syntax hints:   ↔ wb 208   ∧ wa 398   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  3anan12  1092  3ancoma  1094  anandi3  1098  3biant1d  1474  an33rean  1479  an33reanOLD  1480  cad1  1617  3exdistr  1962  ceqsex2  3543  ceqsex2v  3544  ceqsex3v  3545  ceqsex4v  3546  ceqsex6v  3547  ceqsex8v  3548  2reu5lem1  3746  2reu5lem2  3747  2reu5lem3  3748  eldifpr  4597  rexdifpr  4598  trel3  5180  2rbropap  5451  ordelord  6213  dflim2  6247  dff1o4  6623  foco2  6873  brfvopab  7211  ndmovass  7336  ndmovdistr  7337  dflim3  7562  dflim4  7563  mpoxopovel  7886  dfsmo2  7984  dfrecs3  8009  oeeui  8228  ecopovtrn  8400  elixp2  8465  elixp  8468  mptelixpg  8499  eqinf  8948  zorn2lem7  9924  grothprim  10256  grothtsk  10257  divmulasscom  11322  muldivdir  11333  divmuldiv  11340  sup3  11598  dfnn3  11652  prime  12064  eluz2  12250  raluz2  12298  elixx1  12748  elixx3g  12752  elioo2  12780  elioo5  12795  elicc4  12804  iccneg  12859  icoshft  12860  difreicc  12871  elfz1  12898  elfz  12899  elfz2  12900  elfzm11  12979  elfz2nn0  12999  elfzo2  13042  elfzo3  13055  lbfzo0  13078  fzind2  13156  zmodid2  13268  hashgt23el  13786  swrdnd2  14017  swrdnd0  14019  swrdccatin1  14087  swrdccat  14097  repswswrd  14146  swrdco  14199  2swrd2eqwrdeq  14315  ccat2s1fvwALTOLD  14319  rediv  14490  imdiv  14497  cosmul  15526  bitsval  15773  bitsmod  15785  bitscmp  15787  smueqlem  15839  dfgcd2  15894  lcmneg  15947  lcmftp  15980  coprmgcdb  15993  divgcdcoprmex  16010  cncongr1  16011  cncongr2  16012  difsqpwdvds  16223  oddprmdvds  16239  elgz  16267  xpsfrnel  16835  xpsfrnel2  16837  ismre  16861  mreexexlem4d  16918  iscatd2  16952  isssc  17090  eldmcoa  17325  isdrs  17544  isipodrs  17771  mgmsscl  17857  ismhm  17958  mhmpropd  17962  issubm  17968  issubmndb  17970  submacs  17991  issubg  18279  eqglact  18331  eqgid  18332  pgrpsubgsymgbi  18536  isslw  18733  efgsdm  18856  mulgmhm  18948  mulgghm  18949  dmdprd  19120  dprdw  19132  subgdmdprd  19156  dmdprdpr  19171  issrg  19257  srglmhm  19285  srgrmhm  19286  isring  19301  ringlghm  19354  dfrhm2  19469  issubrg3  19563  issdrg  19574  sdrgacs  19580  islmod  19638  lsspropd  19789  islmhm  19799  islbs  19848  lbspropd  19871  isphl  20772  elocv  20812  isobs  20864  mat1dimscm  21084  scmatghm  21142  scmatmhm  21143  ma1repvcl  21179  smadiadetr  21284  mat2pmatghm  21338  mat2pmatmul  21339  decpmatmulsumfsupp  21381  pm2mpghm  21424  pm2mpmhmlem1  21426  neindisj  21725  lmbrf  21868  hauscmplem  22014  llyi  22082  subislly  22089  islocfin  22125  uptx  22233  txcn  22234  qtopeu  22324  elmptrab  22435  isfbas  22437  trfil2  22495  flimcls  22593  cnextcn  22675  xmetec  23044  ngppropd  23246  ngpocelbl  23313  bl2ioo  23400  xrtgioo  23414  om1elbas  23636  elpi1  23649  isclm  23668  isclmp  23701  isncvsngp  23753  iscph  23774  tcphcph  23840  lmmbr2  23862  lmmbrf  23865  iscau2  23880  caussi  23900  lmclim  23906  bcthlem1  23927  srabn  23963  ishl2  23973  evthicc2  24061  ovolfioo  24068  ovolficc  24069  iblcnlem1  24388  iblrelem  24391  iblre  24394  iblcn  24399  isuc1p  24734  ismon1p  24736  ellogrn  25143  logreclem  25340  atandm  25454  atandm2  25455  atandm3  25456  atans2  25509  dmarea  25535  dchrelbas4  25819  lgsmodeq  25918  lgsmulsqcoprm  25919  ax5seg  26724  eengtrkg  26772  uspgredg2v  27006  nb3grpr2  27165  isrusgr0  27348  rusgrprop0  27349  ewlkprop  27385  wksfval  27391  wlkeq  27415  wlkson  27438  wlkonprop  27440  upgr2wlk  27450  upgrtrls  27483  upgristrl  27484  wksonproplem  27486  pthsfval  27502  ispth  27504  isspthonpth  27530  uhgrwkspth  27536  usgr2wlkspth  27540  crctcshwlkn0lem4  27591  wspthnp  27628  wwlknon  27635  wwlksnextwrd  27675  wwlksnextinj  27677  wspthsnwspthsnon  27695  umgr2adedgwlk  27724  umgr2adedgwlkon  27725  umgr2adedgwlkonALT  27726  umgr2adedgspth  27727  s3wwlks2on  27735  wpthswwlks2on  27740  usgr2wspthons3  27743  usgr2wspthon  27744  elwwlks2  27745  elwspths2spth  27746  rusgrnumwwlkl1  27747  rusgrnumwwlkslem  27748  isclwwlk  27762  clwwlkbp  27763  clwlkclwwlklem3  27779  isclwwlknx  27814  clwwlknp  27815  clwwlkn1  27819  clwwlkn2  27822  clwwlkwwlksb  27833  clwwlknonel  27874  0pth  27904  frcond4  28049  1to3vfriswmgr  28059  3cyclfrgr  28067  frgrwopreglem5  28100  2clwwlk2clwwlk  28129  numclwlk1lem1  28148  numclwwlk6  28169  ajval  28638  issh  28985  dmadjss  29664  adjeu  29666  adjval  29667  isst  29990  ishst  29991  xrdifh  30503  nndiffz1  30509  xdivpnfrp  30609  isomnd  30702  isslmd  30830  isprmidl  30955  isprmidlc  30963  ismxidl  30971  isrrext  31241  ismntop  31267  isros  31427  issros  31434  issibf  31591  eulerpartleme  31621  eulerpartlemt0  31627  probun  31677  bnj250  31971  bnj255  31975  bnj345  31984  bnj945  32045  bnj1209  32068  bnj1275  32085  bnj543  32165  bnj571  32178  bnj607  32188  bnj882  32198  bnj983  32223  bnj996  32228  bnj1006  32232  bnj1033  32241  bnj1097  32253  bnj1110  32254  bnj1145  32265  bnj1174  32275  bnj1189  32281  bnj1450  32322  bnj1514  32335  cusgr3cyclex  32383  erdszelem1  32438  cvmsval  32513  cvmliftiota  32548  snmlval  32578  lediv2aALT  32920  elwlim  33110  nocvxminlem  33247  scutcut  33266  scutbday  33267  brtxp2  33342  brpprod3a  33347  brcart  33393  brsuccf  33402  broutsideof3  33587  ivthALT  33683  df3nandALT2  33748  andnand1  33749  topdifinffinlem  34631  relowlssretop  34647  rdgeqoa  34654  unccur  34890  fin2solem  34893  poimirlem3  34910  poimirlem4  34911  poimirlem26  34933  poimirlem27  34934  poimirlem32  34939  itg2gt0cn  34962  iblabsnclem  34970  areacirc  35002  neificl  35043  ablo4pnp  35173  isrngohom  35258  isidl  35307  ispridl  35327  pridlidl  35328  ismaxidl  35333  maxidlidl  35334  isfldidl2  35362  isdmn3  35367  triantru3  35515  moantr  35631  brxrn2  35642  dfxrn2  35643  ecxrn  35654  inxpxrn  35658  rnxrn  35661  islshp  36130  isopos  36331  cvrfval  36419  cvrval  36420  isatl  36450  isat3  36458  islpln5  36686  4atlem11  36760  dalem20  36844  lhpexle3  37163  lhpex2leN  37164  isltrn2N  37271  diclspsn  38345  lcfls1lem  38685  lcfls1N  38686  3cubes  39336  fz1eqin  39415  isdomn3  39853  rp-isfinite6  39933  snhesn  40181  ismnuprim  40679  iotasbc2  40801  eelT00  41088  eelTTT  41089  eelT11  41090  eelT12  41092  eelTT1  41093  eelT01  41094  eel0T1  41095  uun132  41168  uun132p1  41169  un2122  41173  uunTT1  41176  uunTT1p1  41177  uunTT1p2  41178  uunT11  41179  uunT11p1  41180  uunT11p2  41181  uunT12  41182  uunT12p1  41183  uunT12p2  41184  uunT12p3  41185  uunT12p4  41186  uunT12p5  41187  uun111  41188  uun2221  41196  uun2221p1  41197  uun2221p2  41198  stoweidlem17  42351  stoweidlem34  42368  stoweidlem60  42394  ndmaovass  43454  ndmaovdistr  43455  4an21  43518  2elfz3nn0  43565  prproropf1o  43718  fpprel  43942  upwlksfval  44059  isupwlkg  44061  upwlkbprop  44062  isrng  44196  2zrngnmrid  44270  lindslinindsimp2lem5  44566  elpg  44865  alimp-no-surprise  44931