Metamath Proof Explorer


Theorem gt-lth

Description: Relationship between < and > using hypotheses. (Contributed by David A. Wheeler, 19-Apr-2015) (New usage is discouraged.)

Ref Expression
Hypotheses gt-lth.1 A V
gt-lth.2 B V
Assertion gt-lth A > B B < A

Proof

Step Hyp Ref Expression
1 gt-lth.1 A V
2 gt-lth.2 B V
3 df-gt > = < -1
4 3 breqi A > B A < -1 B
5 1 2 brcnv A < -1 B B < A
6 4 5 bitri A > B B < A