theorem eqstr3d (A B C: set) (G: wff): $ G -> B == A $ > $ G -> B == C $ > $ G -> A == C $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqstr3 | B == A -> B == C -> A == C |
|
2 | hyp h1 | G -> B == A |
|
3 | hyp h2 | G -> B == C |
|
4 | 1, 2, 3 | sylc | G -> A == C |