Theorem nleltd

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

	Ref	Expression
Hypotheses	nleltd.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	nleltd.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	nleltd.3	⊢ ( 𝜑 → ¬ 𝐵 ≤ 𝐴 )
Assertion	nleltd	⊢ ( 𝜑 → 𝐴 < 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		nleltd.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		nleltd.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		nleltd.3	⊢ ( 𝜑 → ¬ 𝐵 ≤ 𝐴 )
4	1 2	ltnled	⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ ¬ 𝐵 ≤ 𝐴 ) )
5	3 4	mpbird	⊢ ( 𝜑 → 𝐴 < 𝐵 )