Theorem alrot3

Description: Theorem *11.21 in WhiteheadRussell p. 160. (Contributed by Andrew Salmon, 24-May-2011)

	Ref	Expression
Assertion	alrot3	⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 𝜑 ↔ ∀ 𝑦 ∀ 𝑧 ∀ 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		alcom	⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 ∀ 𝑧 𝜑 )
2		alcom	⊢ ( ∀ 𝑥 ∀ 𝑧 𝜑 ↔ ∀ 𝑧 ∀ 𝑥 𝜑 )
3	2	albii	⊢ ( ∀ 𝑦 ∀ 𝑥 ∀ 𝑧 𝜑 ↔ ∀ 𝑦 ∀ 𝑧 ∀ 𝑥 𝜑 )
4	1 3	bitri	⊢ ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 𝜑 ↔ ∀ 𝑦 ∀ 𝑧 ∀ 𝑥 𝜑 )