Theorem xreqnltd

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

	Ref	Expression
Hypotheses	xreqnltd.1	$$⊢\phi \to A\in {ℝ}^{*}$$
	xreqnltd.2	$$⊢\phi \to A=B$$
Assertion	xreqnltd	$$⊢\phi \to \neg A<B$$

Proof

Step	Hyp	Ref	Expression
1		xreqnltd.1	$$⊢\phi \to A\in {ℝ}^{*}$$
2		xreqnltd.2	$$⊢\phi \to A=B$$
3	2 1	eqeltrrd	$$⊢\phi \to B\in {ℝ}^{*}$$
4		xrlttri3	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A=B\leftrightarrow \left(\neg A<B\wedge \neg B<A\right)\right)$$
5	1 3 4	syl2anc	$$⊢\phi \to \left(A=B\leftrightarrow \left(\neg A<B\wedge \neg B<A\right)\right)$$
6	2 5	mpbid	$$⊢\phi \to \left(\neg A<B\wedge \neg B<A\right)$$
7	6	simpld	$$⊢\phi \to \neg A<B$$