Metamath Proof Explorer
Description: InequalityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020)
|
|
Ref |
Expression |
|
Hypotheses |
int-ineqtransd.1 |
|
|
|
int-ineqtransd.2 |
|
|
|
int-ineqtransd.3 |
|
|
|
int-ineqtransd.4 |
|
|
|
int-ineqtransd.5 |
|
|
Assertion |
int-ineqtransd |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
int-ineqtransd.1 |
|
2 |
|
int-ineqtransd.2 |
|
3 |
|
int-ineqtransd.3 |
|
4 |
|
int-ineqtransd.4 |
|
5 |
|
int-ineqtransd.5 |
|
6 |
3 2 1 5 4
|
letrd |
|