theorem excom {x y: nat} (a: wff x y): $ E. x E. y a -> E. y E. x a $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bi1 | (E. x E. y a <-> E. y E. x a) -> E. x E. y a -> E. y E. x a |
|
2 | excomb | E. x E. y a <-> E. y E. x a |
|
3 | 1, 2 | ax_mp | E. x E. y a -> E. y E. x a |