theorem lelttrd (G: wff) (a b c: nat): $ G -> a <= b $ > $ G -> b < c $ > $ G -> a < c $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lelttr | a <= b -> b < c -> a < c |
|
2 | hyp h1 | G -> a <= b |
|
3 | hyp h2 | G -> b < c |
|
4 | 1, 2, 3 | sylc | G -> a < c |