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

Metamath Proof Explorer

Theorem ltnsym

Description: 'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002)

Ref Expression
Assertion ltnsym ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B → ¬ B < A

Proof

Step Hyp Ref Expression
1 axlttri ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ ¬ A = B ∨ B < A
2 pm2.46 ⊢ ¬ A = B ∨ B < A → ¬ B < A
3 1 2 biimtrdi ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B → ¬ B < A