Metamath Proof Explorer

Theorem alcom

Description: Theorem 19.5 of Margaris p. 89. (Contributed by NM, 30-Jun-1993)

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

Proof

Step Hyp Ref Expression
1 ax-11 
 |-  ( A. x A. y ph -> A. y A. x ph )
2 ax-11 
 |-  ( A. y A. x ph -> A. x A. y ph )
3 1 2 impbii 
 |-  ( A. x A. y ph <-> A. y A. x ph )