theorem alex {x: nat} (a: wff x): $ A. x a <-> ~E. x ~a $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr | (A. x a <-> A. x ~~a) -> (A. x ~~a <-> ~E. x ~a) -> (A. x a <-> ~E. x ~a) |
|
2 | notnot | a <-> ~~a |
|
3 | 2 | aleqi | A. x a <-> A. x ~~a |
4 | 1, 3 | ax_mp | (A. x ~~a <-> ~E. x ~a) -> (A. x a <-> ~E. x ~a) |
5 | alnex | A. x ~~a <-> ~E. x ~a |
|
6 | 4, 5 | ax_mp | A. x a <-> ~E. x ~a |