Theorem 3anass 966

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

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

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 964

This theorem is referenced by:  3anrot  967  3anan12  974  anandi3  975  3exdistr  1887  r3al  2477  ceqsex2  2726  ceqsex3v  2728  ceqsex4v  2729  ceqsex6v  2730  ceqsex8v  2731  trel3  4034  sowlin  4242  dff1o4  5375  mpoxopovel  6138  dfsmo2  6184  ecopovtrn  6526  ecopovtrng  6529  elixp2  6596  elixp  6599  mptelixpg  6628  eqinfti  6907  distrnqg  7195  recmulnqg  7199  ltexnqq  7216  enq0tr  7242  distrnq0  7267  genpdflem  7315  distrlem1prl  7390  distrlem1pru  7391  divmulasscomap  8456  muldivdirap  8467  divmuldivap  8472  prime  9150  eluz2  9332  raluz2  9374  elixx1  9680  elixx3g  9684  elioo2  9704  elioo5  9716  elicc4  9723  iccneg  9772  icoshft  9773  elfz1  9795  elfz  9796  elfz2  9797  elfzm11  9871  elfz2nn0  9892  elfzo2  9927  elfzo3  9940  lbfzo0  9958  fzind2  10016  zmodid2  10125  redivap  10646  imdivap  10653  maxleast  10985  cosmul  11452  dfgcd2  11702  lcmneg  11755  coprmgcdb  11769  divgcdcoprmex  11783  cncongr1  11784  cncongr2  11785  lmbrf  12384  uptx  12443  txcn  12444  xmetec  12606  bl2ioo  12711  findset  13143