Theorem 3anrot 985

Description: Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.)

Assertion

Ref	Expression
3anrot	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))

Proof of Theorem 3anrot

Step	Hyp	Ref	Expression
1		ancom 266	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜑))
2		3anass 984	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		df-3an 982	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜑))
4	1, 2, 3	3bitr4i 212	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))

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

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 982

This theorem is referenced by:  3ancomb  988  3anrev  990  3simpc  998  caovlem2d  6111  nnmcan  6572  modmulconst  11966  srgrmhm  13490  xmetpsmet  14537  comet  14667  lgsdi  15153