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

Metamath Proof Explorer

Theorem ltne

Description: 'Less than' implies not equal. (Contributed by NM, 9-Oct-1999) (Revised by Mario Carneiro, 16-Sep-2015)

		Ref	Expression
	Assertion	ltne	$⊢ (A \in ℝ \land A < B) \to B \neq A$

Step	Hyp	Ref	Expression
1		ltnr	$⊢ A \in ℝ \to \neg A < A$
2		breq2	$⊢ B = A \to (A < B \leftrightarrow A < A)$
3	2	notbid	$⊢ B = A \to (\neg A < B \leftrightarrow \neg A < A)$
4	1 3	syl5ibrcom	$⊢ A \in ℝ \to (B = A \to \neg A < B)$
5	4	necon2ad	$⊢ A \in ℝ \to (A < B \to B \neq A)$
6	5	imp	$⊢ (A \in ℝ \land A < B) \to B \neq A$