Metamath Proof Explorer

Theorem alrot4

Description: Rotate four universal quantifiers twice. (Contributed by NM, 2-Feb-2005) (Proof shortened by Fan Zheng, 6-Jun-2016)

Ref Expression
Assertion alrot4 ⊢ ∀ x ∀ y ∀ z ∀ w φ ↔ ∀ z ∀ w ∀ x ∀ y φ

Proof

Step Hyp Ref Expression
1 alrot3 ⊢ ∀ y ∀ z ∀ w φ ↔ ∀ z ∀ w ∀ y φ
2 1 albii ⊢ ∀ x ∀ y ∀ z ∀ w φ ↔ ∀ x ∀ z ∀ w ∀ y φ
3 alrot3 ⊢ ∀ x ∀ z ∀ w ∀ y φ ↔ ∀ z ∀ w ∀ x ∀ y φ
4 2 3 bitri ⊢ ∀ x ∀ y ∀ z ∀ w φ ↔ ∀ z ∀ w ∀ x ∀ y φ