Theorem truenat | index | src |

theorem truenat (p: wff): $ true (nat p) <-> p $;
StepHypRefExpression
1 con1
(~p -> nat p = 0) -> ~nat p = 0 -> p
2 1 conv ne, true
(~p -> nat p = 0) -> true (nat p) -> p
3 ifneg
~p -> if p 1 0 = 0
4 3 conv nat
~p -> nat p = 0
5 2, 4 ax_mp
true (nat p) -> p
6 d1ne0
1 != 0
7 ifpos
p -> if p 1 0 = 1
8 7 conv nat
p -> nat p = 1
9 8 neeq1d
p -> (nat p != 0 <-> 1 != 0)
10 9 conv true
p -> (true (nat p) <-> 1 != 0)
11 6, 10 mpbiri
p -> true (nat p)
12 5, 11 ibii
true (nat p) <-> p

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid), axs_peano (peano1)