Metamath Proof Explorer


Theorem letri

Description: 'Less than or equal to' is transitive. (Contributed by NM, 14-May-1999)

Ref Expression
Hypotheses lt.1 A
lt.2 B
lt.3 C
Assertion letri A B B C A C

Proof

Step Hyp Ref Expression
1 lt.1 A
2 lt.2 B
3 lt.3 C
4 letr A B C A B B C A C
5 1 2 3 4 mp3an A B B C A C