Theorem d1ne0 ≪ | index | src | ≫

theorem d1ne0: $ 1 != 0 $;

Step	Hyp	Ref	Expression
1		peano1	suc 0 != 0
2	1	conv d1	1 != 0

Axiom use

axs_peano (peano1)