Theorem
b10
≪
|
index
|
src
|
≫
theorem b10: $ b1 0 = 1 $;
Step
Hyp
Ref
Expression
1
suceq
b0 0 = 0 -> suc (b0 0) = suc 0
2
1
conv
b1
,
d1
b0 0 = 0 -> b1 0 = 1
3
b00
b0 0 = 0
4
2
,
3
ax_mp
b1 0 = 1
Axiom use
axs_prop_calc
(
ax_1
,
ax_2
,
ax_3
,
ax_mp
)
,
axs_peano
(
peano2
,
add0
)