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 e. _V
	gt-lth.2	|- B e. _V
Assertion	gt-lth	|- ( A > B <-> B < A )

Proof

Step	Hyp	Ref	Expression
1		gt-lth.1	|- A e. _V
2		gt-lth.2	|- B e. _V
3		df-gt	|- > = `' <
4	3	breqi	|- ( A > B <-> A `' < B )
5	1 2	brcnv	|- ( A `' < B <-> B < A )
6	4 5	bitri	|- ( A > B <-> B < A )