Theorem xrltned

Description: 'Less than' implies not equal. (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	xrltned.1	|- ( ph -> A e. RR* )
	xrltned.2	|- ( ph -> B e. RR* )
	xrltned.3	|- ( ph -> A < B )
Assertion	xrltned	|- ( ph -> A =/= B )

Proof

Step	Hyp	Ref	Expression
1		xrltned.1	|- ( ph -> A e. RR* )
2		xrltned.2	|- ( ph -> B e. RR* )
3		xrltned.3	|- ( ph -> A < B )
4	1 2 3	xrgtned	|- ( ph -> B =/= A )
5	4	necomd	|- ( ph -> A =/= B )