This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xrltned

Description: 'Less than' implies not equal. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses xrltned.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
xrltned.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
xrltned.3 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
Assertion xrltned ( 𝜑 → 𝐴 ≠ 𝐵 )

Proof

Step Hyp Ref Expression
1 xrltned.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2 xrltned.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3 xrltned.3 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
4 1 2 3 xrgtned ⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
5 4 necomd ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )