Metamath Proof Explorer


Theorem letri3i

Description: Consequence of trichotomy. (Contributed by NM, 14-May-1999)

Ref Expression
Hypotheses lt.1 𝐴 ∈ ℝ
lt.2 𝐵 ∈ ℝ
Assertion letri3i ( 𝐴 = 𝐵 ↔ ( 𝐴𝐵𝐵𝐴 ) )

Proof

Step Hyp Ref Expression
1 lt.1 𝐴 ∈ ℝ
2 lt.2 𝐵 ∈ ℝ
3 letri3 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 = 𝐵 ↔ ( 𝐴𝐵𝐵𝐴 ) ) )
4 1 2 3 mp2an ( 𝐴 = 𝐵 ↔ ( 𝐴𝐵𝐵𝐴 ) )