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 𝐴 ∈ V
gte-lteh.2 𝐵 ∈ V
Assertion gte-lteh ( 𝐴𝐵𝐵𝐴 )

Proof

Step Hyp Ref Expression
1 gte-lteh.1 𝐴 ∈ V
2 gte-lteh.2 𝐵 ∈ V
3 df-gte ≥ =
4 3 breqi ( 𝐴𝐵𝐴 𝐵 )
5 1 2 brcnv ( 𝐴 𝐵𝐵𝐴 )
6 4 5 bitri ( 𝐴𝐵𝐵𝐴 )