Theorem gte-lteh

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

	Ref	Expression
Hypotheses	gte-lteh.1	$$⊢A\in \mathrm{V}$$
	gte-lteh.2	$$⊢B\in \mathrm{V}$$
Assertion	gte-lteh	$$⊢A\ge B\leftrightarrow B\le A$$

Proof

Step	Hyp	Ref	Expression
1		gte-lteh.1	$$⊢A\in \mathrm{V}$$
2		gte-lteh.2	$$⊢B\in \mathrm{V}$$
3		df-gte	$$⊢\ge ={\le }^{-1}$$
4	3	breqi	$$⊢A\ge B\leftrightarrow A{\le }^{-1}B$$
5	1 2	brcnv	$$⊢A{\le }^{-1}B\leftrightarrow B\le A$$
6	4 5	bitri	$$⊢A\ge B\leftrightarrow B\le A$$