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 
|- ( A. x A. y A. z A. w ph <-> A. z A. w A. x A. y ph )

Proof

Step Hyp Ref Expression
1 alrot3 
 |-  ( A. y A. z A. w ph <-> A. z A. w A. y ph )
2 1 albii 
 |-  ( A. x A. y A. z A. w ph <-> A. x A. z A. w A. y ph )
3 alrot3 
 |-  ( A. x A. z A. w A. y ph <-> A. z A. w A. x A. y ph )
4 2 3 bitri 
 |-  ( A. x A. y A. z A. w ph <-> A. z A. w A. x A. y ph )