Theorem
true1
≪
|
index
|
src
|
≫
theorem true1: $ true 1 $;
Step
Hyp
Ref
Expression
1
d1ne0
1 != 0
2
1
conv
true
true 1
Axiom use
axs_peano
(
peano1
)