Metamath Proof Explorer


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 AV
gte-lteh.2 BV
Assertion gte-lteh ABBA

Proof

Step Hyp Ref Expression
1 gte-lteh.1 AV
2 gte-lteh.2 BV
3 df-gte =-1
4 3 breqi ABA-1B
5 1 2 brcnv A-1BBA
6 4 5 bitri ABBA