Theorem 3anass 982

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

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

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 980

This theorem is referenced by:  3anrot  983  3anan12  990  anandi3  991  3exdistr  1915  r3al  2521  ceqsex2  2777  ceqsex3v  2779  ceqsex4v  2780  ceqsex6v  2781  ceqsex8v  2782  eldifpr  3619  rexdifpr  3620  trel3  4107  sowlin  4318  dff1o4  5466  mpoxopovel  6237  dfsmo2  6283  ecopovtrn  6627  ecopovtrng  6630  elixp2  6697  elixp  6700  mptelixpg  6729  eqinfti  7014  distrnqg  7381  recmulnqg  7385  ltexnqq  7402  enq0tr  7428  distrnq0  7453  genpdflem  7501  distrlem1prl  7576  distrlem1pru  7577  divmulasscomap  8647  muldivdirap  8658  divmuldivap  8663  prime  9346  eluz2  9528  raluz2  9573  elixx1  9891  elixx3g  9895  elioo2  9915  elioo5  9927  elicc4  9934  iccneg  9983  icoshft  9984  elfz1  10007  elfz  10008  elfz2  10009  elfzm11  10084  elfz2nn0  10105  elfzo2  10143  elfzo3  10156  lbfzo0  10174  fzind2  10232  zmodid2  10345  redivap  10874  imdivap  10881  maxleast  11213  cosmul  11744  dfgcd2  12005  lcmneg  12064  coprmgcdb  12078  divgcdcoprmex  12092  cncongr1  12093  cncongr2  12094  difsqpwdvds  12327  elgz  12359  mgmsscl  12710  ismhm  12781  mhmpropd  12785  issubm  12791  issubg  12960  issrg  13048  srglmhm  13076  srgrmhm  13077  isring  13083  lmbrf  13497  uptx  13556  txcn  13557  xmetec  13719  bl2ioo  13824  lgsmodeq  14228  lgsmulsqcoprm  14229  findset  14468