Metamath Proof Explorer


Theorem int-ineqtransd

Description: InequalityTransitivity generator rule. (Contributed by Stanislas Polu, 7-Apr-2020)

Ref Expression
Hypotheses int-ineqtransd.1 φ A
int-ineqtransd.2 φ B
int-ineqtransd.3 φ C
int-ineqtransd.4 φ B A
int-ineqtransd.5 φ C B
Assertion int-ineqtransd φ C A

Proof

Step Hyp Ref Expression
1 int-ineqtransd.1 φ A
2 int-ineqtransd.2 φ B
3 int-ineqtransd.3 φ C
4 int-ineqtransd.4 φ B A
5 int-ineqtransd.5 φ C B
6 3 2 1 5 4 letrd φ C A