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 φBA
int-ineqtransd.5 φCB
Assertion int-ineqtransd φCA

Proof

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