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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-11 | ||
2 | ax-11 | ||
3 | 1 2 | impbii |