Theorem d2ne0 ≪ | index | src | ≫

theorem d2ne0: $ 2 != 0 $;

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

Axiom use

axs_peano (peano1)