Metamath Proof Explorer


Theorem leltned

Description: 'Less than or equal to' implies 'less than' is not 'equals'. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses ltd.1 φA
ltd.2 φB
leltned.3 φAB
Assertion leltned φA<BBA

Proof

Step Hyp Ref Expression
1 ltd.1 φA
2 ltd.2 φB
3 leltned.3 φAB
4 leltne ABABA<BBA
5 1 2 3 4 syl3anc φA<BBA