theorem syl5eqs (A B C: set) (G: wff):
$ A == B $ >
$ G -> B == C $ >
$ G -> A == C $;
Step | Hyp | Ref | Expression |
1 |
|
hyp h1 |
A == B |
2 |
1 |
a1i |
G -> A == B |
3 |
|
hyp h2 |
G -> B == C |
4 |
2, 3 |
eqstrd |
G -> A == C |
Axiom use
axs_prop_calc
(ax_1,
ax_2,
ax_3,
ax_mp),
axs_pred_calc
(ax_gen,
ax_4)