Metamath Proof Explorer


Theorem int-ineq1stprincd

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

Ref Expression
Hypotheses int-ineq1stprincd.1 φ A
int-ineq1stprincd.2 φ B
int-ineq1stprincd.3 φ C
int-ineq1stprincd.4 φ D
int-ineq1stprincd.5 φ B A
int-ineq1stprincd.6 φ D C
Assertion int-ineq1stprincd φ B + D A + C

Proof

Step Hyp Ref Expression
1 int-ineq1stprincd.1 φ A
2 int-ineq1stprincd.2 φ B
3 int-ineq1stprincd.3 φ C
4 int-ineq1stprincd.4 φ D
5 int-ineq1stprincd.5 φ B A
6 int-ineq1stprincd.6 φ D C
7 2 4 1 3 5 6 le2addd φ B + D A + C