Metamath Proof Explorer

Theorem alrot3

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

Ref Expression
Assertion alrot3 
|- ( A. x A. y A. z ph <-> A. y A. z A. x ph )

Proof

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