Theorem sstr ≪ | index | src | ≫ 

theorem sstr (A B C: set): $ A C_ B -> B C_ C -> A C_ C $;
StepHypRefExpression
1 ssel 
A C_ B -> x e. A -> x e. B
2 1 anwl 
A C_ B /\ B C_ C -> x e. A -> x e. B
3 ssel 
B C_ C -> x e. B -> x e. C
4 3 anwr 
A C_ B /\ B C_ C -> x e. B -> x e. C
5 2, 4 syld 
A C_ B /\ B C_ C -> x e. A -> x e. C
6 5 iald 
A C_ B /\ B C_ C -> A. x (x e. A -> x e. C)
7 6 conv subset 
A C_ B /\ B C_ C -> A C_ C
8 7 exp 
A C_ B -> B C_ C -> A C_ C

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_12), axs_set (ax_8)