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)