Metamath Proof Explorer
Description: 'Less than' implies not equal. (Contributed by Mario Carneiro, 30Sep2013)


Ref 
Expression 

Hypotheses 
lt.1 
$${\u22a2}{A}\in \mathbb{R}$$ 


ltneii.2 
$${\u22a2}{A}<{B}$$ 

Assertion 
gtneii 
$${\u22a2}{B}\ne {A}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

lt.1 
$${\u22a2}{A}\in \mathbb{R}$$ 
2 

ltneii.2 
$${\u22a2}{A}<{B}$$ 
3 

ltne 
$${\u22a2}\left({A}\in \mathbb{R}\wedge {A}<{B}\right)\to {B}\ne {A}$$ 
4 
1 2 3

mp2an 
$${\u22a2}{B}\ne {A}$$ 