Theorem ltneii

Description: 'Greater than' implies not equal. (Contributed by Mario Carneiro, 16-Sep-2015)

	Ref	Expression
Hypotheses	lt.1	$$⊢A\in ℝ$$
	ltneii.2	$$⊢A<B$$
Assertion	ltneii	$$⊢A\ne B$$

Proof

Step	Hyp	Ref	Expression
1		lt.1	$$⊢A\in ℝ$$
2		ltneii.2	$$⊢A<B$$
3	1 2	gtneii	$$⊢B\ne A$$
4	3	necomi	$$⊢A\ne B$$