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

Metamath Proof Explorer

Theorem xrgtned

Description: 'Greater than' implies not equal. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses xrgtned.1 ⊢ φ → A ∈ ℝ *
xrgtned.2 ⊢ φ → B ∈ ℝ *
xrgtned.3 ⊢ φ → A < B
Assertion xrgtned ⊢ φ → B ≠ A

Proof

Step Hyp Ref Expression
1 xrgtned.1 ⊢ φ → A ∈ ℝ *
2 xrgtned.2 ⊢ φ → B ∈ ℝ *
3 xrgtned.3 ⊢ φ → A < B
4 xrltne ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A < B → B ≠ A
5 1 2 3 4 syl3anc ⊢ φ → B ≠ A