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