Metamath Proof Explorer


Theorem leid

Description: 'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999)

Ref Expression
Assertion leid AAA

Proof

Step Hyp Ref Expression
1 eqid A=A
2 1 olci A<AA=A
3 leloe AAAAA<AA=A
4 2 3 mpbiri AAAA
5 4 anidms AAA