Theorem muleqd | index | src |

theorem muleqd (G: wff) (a b c d: nat):
  $ G -> a = b $ >
  $ G -> c = d $ >
  $ G -> a * c = b * d $;
StepHypRefExpression
1 muleq
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 (muleq)