Theorem 3anass 971

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 969	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		anass 399	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3	1, 2	bitri 183	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

Syntax hints:   ∧ wa 103   ↔ wb 104   ∧ w3a 967

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

This theorem depends on definitions:  df-bi 116  df-3an 969

This theorem is referenced by:  3anrot  972  3anan12  979  anandi3  980  3exdistr  1902  r3al  2508  ceqsex2  2761  ceqsex3v  2763  ceqsex4v  2764  ceqsex6v  2765  ceqsex8v  2766  eldifpr  3597  rexdifpr  3598  trel3  4082  sowlin  4292  dff1o4  5434  mpoxopovel  6200  dfsmo2  6246  ecopovtrn  6589  ecopovtrng  6592  elixp2  6659  elixp  6662  mptelixpg  6691  eqinfti  6976  distrnqg  7319  recmulnqg  7323  ltexnqq  7340  enq0tr  7366  distrnq0  7391  genpdflem  7439  distrlem1prl  7514  distrlem1pru  7515  divmulasscomap  8583  muldivdirap  8594  divmuldivap  8599  prime  9281  eluz2  9463  raluz2  9508  elixx1  9824  elixx3g  9828  elioo2  9848  elioo5  9860  elicc4  9867  iccneg  9916  icoshft  9917  elfz1  9940  elfz  9941  elfz2  9942  elfzm11  10016  elfz2nn0  10037  elfzo2  10075  elfzo3  10088  lbfzo0  10106  fzind2  10164  zmodid2  10277  redivap  10802  imdivap  10809  maxleast  11141  cosmul  11672  dfgcd2  11932  lcmneg  11985  coprmgcdb  11999  divgcdcoprmex  12013  cncongr1  12014  cncongr2  12015  difsqpwdvds  12246  lmbrf  12756  uptx  12815  txcn  12816  xmetec  12978  bl2ioo  13083  findset  13662