theorem b0eqd (_G: wff) (_n1 _n2: nat):
$ _G -> _n1 = _n2 $ >
$ _G -> b0 _n1 = b0 _n2 $;
| Step | Hyp | Ref | Expression |
|---|
| 1 |
|
hyp _nh |
_G -> _n1 = _n2 |
| 2 |
1, 1 |
addeqd |
_G -> _n1 + _n1 = _n2 + _n2 |
| 3 |
2 |
conv b0 |
_G -> b0 _n1 = b0 _n2 |
Axiom use
axs_prop_calc
(ax_1,
ax_2,
ax_mp),
axs_peano
(addeq)