theorem ltletrd (G: wff) (a b c: nat): $ G -> a < b $ > $ G -> b <= c $ > $ G -> a < c $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hyp h1 | G -> a < b |
|
2 | 1 | conv lt | G -> suc a <= b |
3 | hyp h2 | G -> b <= c |
|
4 | 2, 3 | letrd | G -> suc a <= c |
5 | 4 | conv lt | G -> a < c |