Theorem nleltd

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

	Ref	Expression
Hypotheses	nleltd.1	|- ( ph -> A e. RR )
	nleltd.2	|- ( ph -> B e. RR )
	nleltd.3	|- ( ph -> -. B <_ A )
Assertion	nleltd	|- ( ph -> A < B )

Proof

Step	Hyp	Ref	Expression
1		nleltd.1	|- ( ph -> A e. RR )
2		nleltd.2	|- ( ph -> B e. RR )
3		nleltd.3	|- ( ph -> -. B <_ A )
4	1 2	ltnled	|- ( ph -> ( A < B <-> -. B <_ A ) )
5	3 4	mpbird	|- ( ph -> A < B )