Metamath Proof Explorer


Theorem lttri5d

Description: Not equal and not larger implies smaller. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses lttri5d.a φA
lttri5d.b φB
lttri5d.aneb φAB
lttri5d.nlt φ¬B<A
Assertion lttri5d φA<B

Proof

Step Hyp Ref Expression
1 lttri5d.a φA
2 lttri5d.b φB
3 lttri5d.aneb φAB
4 lttri5d.nlt φ¬B<A
5 1 rexrd φA*
6 2 rexrd φB*
7 5 6 3 4 xrlttri5d φA<B