Theorem b00 ≪ | index | src | ≫

theorem b00: $ b0 0 = 0 $;

Step	Hyp	Ref	Expression
1		add0	0 + 0 = 0
2	1	conv b0	b0 0 = 0

Axiom use

axs_peano (add0)