Theorem xrltnled

Description: 'Less than' in terms of 'less than or equal to'. (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	xrltnled.1	$$⊢\phi \to A\in {ℝ}^{*}$$
	xrltnled.2	$$⊢\phi \to B\in {ℝ}^{*}$$
Assertion	xrltnled	$$⊢\phi \to \left(A<B\leftrightarrow \neg B\le A\right)$$

Proof

Step	Hyp	Ref	Expression
1		xrltnled.1	$$⊢\phi \to A\in {ℝ}^{*}$$
2		xrltnled.2	$$⊢\phi \to B\in {ℝ}^{*}$$
3		xrltnle	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A<B\leftrightarrow \neg B\le A\right)$$
4	1 2 3	syl2anc	$$⊢\phi \to \left(A<B\leftrightarrow \neg B\le A\right)$$