Theorem true1 | index | src |

theorem true1: $ true 1 $;
StepHypRefExpression
1 d1ne0
1 != 0
2 1 conv true
true 1

Axiom use

axs_peano (peano1)