Theorem syl5eqr ≪ | index | src | ≫

theorem syl5eqr (G: wff) (a b c: nat):
  $ b = a $ >
  $ G -> b = c $ >
  $ G -> a = c $;

Step	Hyp	Ref	Expression
1		hyp h1	b = a
2	1	a1i	G -> b = a
3		hyp h2	G -> b = c
4	2, 3	eqtr3d	G -> a = c

Axiom use

axs_prop_calc (ax_1, ax_2, ax_mp), axs_pred_calc (ax_7)