theorem eal {x: nat} (a: wff x): $ A. x a -> a $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax_3 | (~a -> ~A. x a) -> A. x a -> a |
|
2 | exnal | E. x ~a <-> ~A. x a |
|
3 | iex | ~a -> E. x ~a |
|
4 | 2, 3 | sylib | ~a -> ~A. x a |
5 | 1, 4 | ax_mp | A. x a -> a |