Metamath Proof Explorer

Theorem leidi

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

Ref Expression
Hypothesis lt2.1 
|- A e. RR
Assertion leidi 
|- A <_ A

Proof

Step Hyp Ref Expression
1 lt2.1 
 |-  A e. RR
2 leid 
 |-  ( A e. RR -> A <_ A )
3 1 2 ax-mp 
 |-  A <_ A