Theorem xreqnltd

Description: A consequence of trichotomy. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step	Hyp	Ref	Expression
1		xreqnltd.1	|- ( ph -> A e. RR* )
2		xreqnltd.2	|- ( ph -> A = B )
3	2 1	eqeltrrd	|- ( ph -> B e. RR* )
4		xrlttri3	|- ( ( A e. RR* /\ B e. RR* ) -> ( A = B <-> ( -. A < B /\ -. B < A ) ) )
5	1 3 4	syl2anc	|- ( ph -> ( A = B <-> ( -. A < B /\ -. B < A ) ) )
6	2 5	mpbid	|- ( ph -> ( -. A < B /\ -. B < A ) )
7	6	simpld	|- ( ph -> -. A < B )