theorem syl5eqsr (A B C: set) (G: wff):
$ 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 |
eqstr3d |
G -> A == C |
Axiom use
axs_prop_calc
(ax_1,
ax_2,
ax_3,
ax_mp),
axs_pred_calc
(ax_gen,
ax_4)