Metamath Proof Explorer


Theorem gt-lt

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

Ref Expression
Assertion gt-lt AVBVA>BB<A

Proof

Step Hyp Ref Expression
1 df-gt >=<-1
2 1 breqi A>BA<-1B
3 brcnvg AVBVA<-1BB<A
4 2 3 bitrid AVBVA>BB<A