Theorem addeqd | index | src |

theorem addeqd (G: wff) (a b c d: nat):
  $ G -> a = b $ >
  $ G -> c = d $ >
  $ G -> a + c = b + d $;
StepHypRefExpression
1 addeq
a = b -> c = d -> a + c = b + d
2 hyp h1
G -> a = b
3 hyp h2
G -> c = d
4 1, 2, 3 sylc
G -> a + c = b + d

Axiom use

axs_prop_calc (ax_1, ax_2, ax_mp), axs_peano (addeq)