Theorem 3anass 938

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 936	. 2 ⊢ ((φ ∧ ψ ∧ χ) ↔ ((φ ∧ ψ) ∧ χ))
2		anass 630	. 2 ⊢ (((φ ∧ ψ) ∧ χ) ↔ (φ ∧ (ψ ∧ χ)))
3	1, 2	bitri 240	1 ⊢ ((φ ∧ ψ ∧ χ) ↔ (φ ∧ (ψ ∧ χ)))

Syntax hints:   ↔ wb 176   ∧ wa 358   ∧ w3a 934

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 177  df-an 360  df-3an 936

This theorem is referenced by:  3anrot  939  3anan12  947  3exdistr  1910  r3al  2672  ceqsex2  2896  ceqsex3v  2898  ceqsex4v  2899  ceqsex6v  2900  ceqsex8v  2901  2reu5lem1  3042  2reu5lem2  3043  2reu5lem3  3044  otkelins2kg  4254  otkelins3kg  4255  opkelcokg  4262  setconslem1  4732  dff1o2  5292  dff1o4  5295  dmsi  5520  ndmovass  5619  ndmovdistr  5620  brsnsi1  5776  brsnsi2  5777  brtxp  5784  restxp  5787  oqelins4  5795  dmtxp  5803  brpprod  5840  dmpprod  5841  xpassenlem  6057  xpassen  6058  ceex  6175  ce0nnul  6178  spacind  6288