Theorem nleltd

Description: 'Not less than or equal to' implies 'grater than'. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	nleltd.1	$$⊢\phi \to A\in ℝ$$
	nleltd.2	$$⊢\phi \to B\in ℝ$$
	nleltd.3	$$⊢\phi \to \neg B\le A$$
Assertion	nleltd	$$⊢\phi \to A<B$$

Proof

Step	Hyp	Ref	Expression
1		nleltd.1	$$⊢\phi \to A\in ℝ$$
2		nleltd.2	$$⊢\phi \to B\in ℝ$$
3		nleltd.3	$$⊢\phi \to \neg B\le A$$
4	1 2	ltnled	$$⊢\phi \to \left(A<B\leftrightarrow \neg B\le A\right)$$
5	3 4	mpbird	$$⊢\phi \to A<B$$