Theorem d2ne0 | index | src |

theorem d2ne0: $ 2 != 0 $;
StepHypRefExpression
1 peano1
suc 1 != 0
2 1 conv d2
2 != 0

Axiom use

axs_peano (peano1)