theorem exal {x y: nat} (a: wff x y): $ E. x A. y a -> A. y E. x a $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfex1 | F/ x E. x a |
|
2 | 1 | nfal | F/ x A. y E. x a |
3 | iex | a -> E. x a |
|
4 | 3 | alimi | A. y a -> A. y E. x a |
5 | 2, 4 | eexh | E. x A. y a -> A. y E. x a |