Metamath Proof Explorer


Theorem alcom

Description: Theorem 19.5 of Margaris p. 89. Use its weak version alcomw when it allows to avoid dependence on ax-11 . (Contributed by NM, 30-Jun-1993)

Ref Expression
Assertion alcom x y φ y x φ

Proof

Step Hyp Ref Expression
1 ax-11 x y φ y x φ
2 ax-11 y x φ x y φ
3 1 2 impbii x y φ y x φ