Theorem lttri5d

Description: Not equal and not larger implies smaller. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	lttri5d.a	$$⊢\phi \to A\in ℝ$$
	lttri5d.b	$$⊢\phi \to B\in ℝ$$
	lttri5d.aneb	$$⊢\phi \to A\ne B$$
	lttri5d.nlt	$$⊢\phi \to \neg B<A$$
Assertion	lttri5d	$$⊢\phi \to A<B$$

Proof

Step	Hyp	Ref	Expression
1		lttri5d.a	$$⊢\phi \to A\in ℝ$$
2		lttri5d.b	$$⊢\phi \to B\in ℝ$$
3		lttri5d.aneb	$$⊢\phi \to A\ne B$$
4		lttri5d.nlt	$$⊢\phi \to \neg B<A$$
5	1	rexrd	$$⊢\phi \to A\in {ℝ}^{*}$$
6	2	rexrd	$$⊢\phi \to B\in {ℝ}^{*}$$
7	5 6 3 4	xrlttri5d	$$⊢\phi \to A<B$$