Theorem xrleneltd

Description: 'Less than or equal to' and 'not equals' implies 'less than', for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	xrleneltd.a	$$⊢\phi \to A\in {ℝ}^{*}$$
	xrleneltd.b	$$⊢\phi \to B\in {ℝ}^{*}$$
	xrleneltd.alb	$$⊢\phi \to A\le B$$
	xrleneltd.anb	$$⊢\phi \to A\ne B$$
Assertion	xrleneltd	$$⊢\phi \to A<B$$

Proof

Step	Hyp	Ref	Expression
1		xrleneltd.a	$$⊢\phi \to A\in {ℝ}^{*}$$
2		xrleneltd.b	$$⊢\phi \to B\in {ℝ}^{*}$$
3		xrleneltd.alb	$$⊢\phi \to A\le B$$
4		xrleneltd.anb	$$⊢\phi \to A\ne B$$
5	4	necomd	$$⊢\phi \to B\ne A$$
6		xrleltne	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\wedge A\le B\right)\to \left(A<B\leftrightarrow B\ne A\right)$$
7	1 2 3 6	syl3anc	$$⊢\phi \to \left(A<B\leftrightarrow B\ne A\right)$$
8	5 7	mpbird	$$⊢\phi \to A<B$$