theorem eqtr3g (G: wff) (a b c d: nat): $ a = c $ > $ b = d $ > $ G -> a = b $ > $ G -> c = d $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hyp h1 | a = c |
|
2 | hyp h2 | b = d |
|
3 | hyp h | G -> a = b |
|
4 | 2, 3 | syl6eq | G -> a = d |
5 | 1, 4 | syl5eqr | G -> c = d |