theorem nateq0 (p: wff): $ nat p = 0 <-> ~p $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | con2b | (p <-> ~nat p = 0) -> (nat p = 0 <-> ~p) |
|
2 | bicom | (~nat p = 0 <-> p) -> (p <-> ~nat p = 0) |
|
3 | truenat | true (nat p) <-> p |
|
4 | 3 | conv ne, true | ~nat p = 0 <-> p |
5 | 2, 4 | ax_mp | p <-> ~nat p = 0 |
6 | 1, 5 | ax_mp | nat p = 0 <-> ~p |