Metamath Proof Explorer


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 )