theorem lteqd (_G: wff) (_a1 _a2 _b1 _b2: nat): $ _G -> _a1 = _a2 $ > $ _G -> _b1 = _b2 $ > $ _G -> (_a1 < _b1 <-> _a2 < _b2) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hyp _ah | _G -> _a1 = _a2 |
|
2 | 1 | suceqd | _G -> suc _a1 = suc _a2 |
3 | hyp _bh | _G -> _b1 = _b2 |
|
4 | 2, 3 | leeqd | _G -> (suc _a1 <= _b1 <-> suc _a2 <= _b2) |
5 | 4 | conv lt | _G -> (_a1 < _b1 <-> _a2 < _b2) |