Theorem 3anass 1009

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 1007	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		anass 401	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3	1, 2	bitri 184	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

Syntax hints:   ∧ wa 104   ↔ wb 105   ∧ w3a 1005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  3anrot  1010  3anan12  1017  anandi3  1018  3biant1d  1392  3exdistr  1965  r3al  2586  ceqsex2  2855  ceqsex3v  2857  ceqsex4v  2858  ceqsex6v  2859  ceqsex8v  2860  eldifpr  3716  rexdifpr  3717  trel3  4216  sowlin  4441  dff1o4  5622  mpoxopovel  6472  dfsmo2  6518  ecopovtrn  6866  ecopovtrng  6869  elixp2  6937  elixp  6940  mptelixpg  6969  eqinfti  7311  distrnqg  7702  recmulnqg  7706  ltexnqq  7723  enq0tr  7749  distrnq0  7774  genpdflem  7822  distrlem1prl  7897  distrlem1pru  7898  divmulasscomap  8970  muldivdirap  8981  divmuldivap  8986  prime  9677  eluz2  9859  raluz2  9911  elixx1  10230  elixx3g  10234  elioo2  10254  elioo5  10266  elicc4  10273  iccneg  10322  icoshft  10323  elfz1  10347  elfz  10348  elfz2  10349  elfzm11  10425  elfz2nn0  10446  elfzo2  10484  elfzo3  10498  lbfzo0  10519  fzind2  10585  zmodid2  10714  swrdccatin1  11417  swrdccat  11427  redivap  11559  imdivap  11566  maxleast  11898  cosmul  12431  bitsval  12629  bitsmod  12642  bitscmp  12644  dfgcd2  12710  lcmneg  12771  coprmgcdb  12785  divgcdcoprmex  12799  cncongr1  12800  cncongr2  12801  difsqpwdvds  13036  elgz  13069  xpsfrnel  13557  xpsfrnel2  13559  mgmsscl  13574  ismhm  13674  mhmpropd  13679  issubm  13685  issubg  13890  eqglact  13942  eqgid  13943  ecqusaddd  13955  ecqusaddcl  13956  isrng  14078  issrg  14109  srglmhm  14137  srgrmhm  14138  isring  14144  ringlghm  14205  dfrhm2  14299  issubrng  14344  issubrg3  14392  islmod  14439  islssm  14505  islssmg  14506  lsspropdg  14579  qusmulrng  14680  lmbrf  15080  uptx  15139  txcn  15140  xmetec  15302  bl2ioo  15415  lgsmodeq  15918  lgsmulsqcoprm  15919  uspgredg2v  16216  wksfval  16317  wlkeq  16349  isclwwlk  16389  clwwlkbp  16390  isclwwlknx  16411  clwwlknp  16412  clwwlkn1  16413  clwwlkn2  16416  clwwlknonel  16427  findset  16715