Theorem 3anass 1093

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

Syntax hints:   ↔ wb 205   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  3anan12  1094  3ancoma  1096  anandi3  1100  3biant1d  1476  an33rean  1481  an33reanOLD  1482  cad1  1620  3exdistr  1965  ceqsex2  3472  ceqsex2v  3473  ceqsex3v  3474  ceqsex4v  3475  ceqsex6v  3476  ceqsex8v  3477  2reu5lem1  3685  2reu5lem2  3686  2reu5lem3  3687  eldifpr  4590  rexdifpr  4591  trel3  5195  2rbropap  5470  ordelord  6273  dflim2  6307  dff1o4  6708  foco2  6965  brfvopab  7310  eloprabga  7360  ndmovass  7438  ndmovdistr  7439  dflim3  7669  dflim4  7670  mpoxopovel  8007  dfsmo2  8149  dfrecs3  8174  dfrecs3OLD  8175  oeeui  8395  ecopovtrn  8567  elixp2  8647  elixp  8650  mptelixpg  8681  dif1en  8907  ssfi  8918  sbthfilem  8941  eqinf  9173  zorn2lem7  10189  grothprim  10521  grothtsk  10522  divmulasscom  11587  muldivdir  11598  divmuldiv  11605  sup3  11862  dfnn3  11917  prime  12331  eluz2  12517  raluz2  12566  elixx1  13017  elixx3g  13021  elioo2  13049  elioo5  13065  elicc4  13075  iccneg  13133  icoshft  13134  difreicc  13145  elfz1  13173  elfz  13174  elfz2  13175  elfzm11  13256  elfz2nn0  13276  elfzo2  13319  elfzo3  13332  lbfzo0  13355  fzind2  13433  zmodid2  13547  hashgt23el  14067  swrdnd2  14296  swrdnd0  14298  swrdccatin1  14366  swrdccat  14376  repswswrd  14425  swrdco  14478  2swrd2eqwrdeq  14594  ccat2s1fvwALTOLD  14598  rediv  14770  imdiv  14777  cosmul  15810  bitsval  16059  bitsmod  16071  bitscmp  16073  smueqlem  16125  dfgcd2  16182  lcmneg  16236  lcmftp  16269  coprmgcdb  16282  divgcdcoprmex  16299  cncongr1  16300  cncongr2  16301  difsqpwdvds  16516  oddprmdvds  16532  elgz  16560  xpsfrnel  17190  xpsfrnel2  17192  ismre  17216  mreexexlem4d  17273  iscatd2  17307  isssc  17449  eldmcoa  17696  isdrs  17934  isipodrs  18170  mgmsscl  18246  ismhm  18347  mhmpropd  18351  issubm  18357  issubmndb  18359  submacs  18380  issubg  18670  eqglact  18722  eqgid  18723  pgrpsubgsymgbi  18931  isslw  19128  efgsdm  19251  mulgmhm  19344  mulgghm  19345  dmdprd  19516  dprdw  19528  subgdmdprd  19552  dmdprdpr  19567  issrg  19658  srglmhm  19686  srgrmhm  19687  isring  19702  ringlghm  19758  dfrhm2  19876  issubrg3  19967  issdrg  19978  sdrgacs  19984  islmod  20042  lsspropd  20194  islmhm  20204  islbs  20253  lbspropd  20276  isphl  20745  elocv  20785  isobs  20837  mat1dimscm  21532  scmatghm  21590  scmatmhm  21591  ma1repvcl  21627  smadiadetr  21732  mat2pmatghm  21787  mat2pmatmul  21788  decpmatmulsumfsupp  21830  pm2mpghm  21873  pm2mpmhmlem1  21875  neindisj  22176  lmbrf  22319  hauscmplem  22465  llyi  22533  subislly  22540  islocfin  22576  uptx  22684  txcn  22685  qtopeu  22775  elmptrab  22886  isfbas  22888  trfil2  22946  flimcls  23044  cnextcn  23126  xmetec  23495  ngppropd  23699  ngpocelbl  23774  bl2ioo  23861  xrtgioo  23875  om1elbas  24101  elpi1  24114  isclm  24133  isclmp  24166  isncvsngp  24218  iscph  24239  tcphcph  24306  lmmbr2  24328  lmmbrf  24331  iscau2  24346  caussi  24366  lmclim  24372  bcthlem1  24393  srabn  24429  ishl2  24439  evthicc2  24529  ovolfioo  24536  ovolficc  24537  iblcnlem1  24857  iblrelem  24860  iblre  24863  iblcn  24868  isuc1p  25210  ismon1p  25212  ellogrn  25620  logreclem  25817  atandm  25931  atandm2  25932  atandm3  25933  atans2  25986  dmarea  26012  dchrelbas4  26296  lgsmodeq  26395  lgsmulsqcoprm  26396  ax5seg  27209  eengtrkg  27257  uspgredg2v  27494  nb3grpr2  27653  isrusgr0  27836  rusgrprop0  27837  ewlkprop  27873  wksfval  27879  wlkeq  27903  wlkson  27926  wlkonprop  27928  upgr2wlk  27938  upgrtrls  27971  upgristrl  27972  wksonproplem  27974  pthsfval  27990  ispth  27992  isspthonpth  28018  uhgrwkspth  28024  usgr2wlkspth  28028  crctcshwlkn0lem4  28079  wspthnp  28116  wwlknon  28123  wwlksnextwrd  28163  wwlksnextinj  28165  wspthsnwspthsnon  28182  umgr2adedgwlk  28211  umgr2adedgwlkon  28212  umgr2adedgwlkonALT  28213  umgr2adedgspth  28214  s3wwlks2on  28222  wpthswwlks2on  28227  usgr2wspthons3  28230  usgr2wspthon  28231  elwwlks2  28232  elwspths2spth  28233  rusgrnumwwlkl1  28234  rusgrnumwwlkslem  28235  isclwwlk  28249  clwwlkbp  28250  clwlkclwwlklem3  28266  isclwwlknx  28301  clwwlknp  28302  clwwlkn1  28306  clwwlkn2  28309  clwwlkwwlksb  28319  clwwlknonel  28360  0pth  28390  frcond4  28535  1to3vfriswmgr  28545  3cyclfrgr  28553  frgrwopreglem5  28586  2clwwlk2clwwlk  28615  numclwlk1lem1  28634  numclwwlk6  28655  ajval  29124  issh  29471  dmadjss  30150  adjeu  30152  adjval  30153  isst  30476  ishst  30477  xrdifh  31003  nndiffz1  31009  xdivpnfrp  31109  isomnd  31229  isslmd  31357  isprmidl  31515  isprmidlc  31525  ismxidl  31536  isrrext  31850  ismntop  31876  isros  32036  issros  32043  issibf  32200  eulerpartleme  32230  eulerpartlemt0  32236  probun  32286  bnj250  32580  bnj255  32584  bnj345  32593  bnj945  32653  bnj1209  32676  bnj1275  32693  bnj543  32773  bnj571  32786  bnj607  32796  bnj882  32806  bnj983  32831  bnj996  32836  bnj1006  32840  bnj1033  32849  bnj1097  32861  bnj1110  32862  bnj1145  32873  bnj1174  32883  bnj1189  32889  bnj1450  32930  bnj1514  32943  cusgr3cyclex  32998  erdszelem1  33053  cvmsval  33128  cvmliftiota  33163  snmlval  33193  lediv2aALT  33535  frxp2  33718  elwlim  33744  nocvxminlem  33899  scutcut  33922  scutbday  33925  brtxp2  34110  brpprod3a  34115  brcart  34161  brsuccf  34170  broutsideof3  34355  ivthALT  34451  df3nandALT2  34516  andnand1  34517  topdifinffinlem  35445  relowlssretop  35461  rdgeqoa  35468  unccur  35687  fin2solem  35690  poimirlem3  35707  poimirlem4  35708  poimirlem26  35730  poimirlem27  35731  poimirlem32  35736  itg2gt0cn  35759  iblabsnclem  35767  areacirc  35797  neificl  35838  ablo4pnp  35965  isrngohom  36050  isidl  36099  ispridl  36119  pridlidl  36120  ismaxidl  36125  maxidlidl  36126  isfldidl2  36154  isdmn3  36159  triantru3  36307  moantr  36421  brxrn2  36432  dfxrn2  36433  ecxrn  36444  inxpxrn  36448  rnxrn  36451  islshp  36920  isopos  37121  cvrfval  37209  cvrval  37210  isatl  37240  isat3  37248  islpln5  37476  4atlem11  37550  dalem20  37634  lhpexle3  37953  lhpex2leN  37954  isltrn2N  38061  diclspsn  39135  lcfls1lem  39475  lcfls1N  39476  uzindd  39913  flt4lem5e  40409  3cubes  40428  fz1eqin  40507  isdomn3  40945  rp-isfinite6  41023  snhesn  41283  ismnuprim  41801  ismnushort  41808  iotasbc2  41927  eelT00  42214  eelTTT  42215  eelT11  42216  eelT12  42218  eelTT1  42219  eelT01  42220  eel0T1  42221  uun132  42294  uun132p1  42295  un2122  42299  uunTT1  42302  uunTT1p1  42303  uunTT1p2  42304  uunT11  42305  uunT11p1  42306  uunT11p2  42307  uunT12  42308  uunT12p1  42309  uunT12p2  42310  uunT12p3  42311  uunT12p4  42312  uunT12p5  42313  uun111  42314  uun2221  42322  uun2221p1  42323  uun2221p2  42324  stoweidlem17  43448  stoweidlem34  43465  stoweidlem60  43491  ndmaovass  44585  ndmaovdistr  44586  4an21  44649  2elfz3nn0  44696  prproropf1o  44847  fpprel  45068  upwlksfval  45185  isupwlkg  45187  upwlkbprop  45188  isrng  45322  2zrngnmrid  45396  lindslinindsimp2lem5  45691  i0oii  46101  io1ii  46102  sepnsepolem1  46103  iscnrm3lem3  46117  isthincd2  46207  functhinc  46214  elpg  46305  alimp-no-surprise  46371