Metamath Proof Explorer

Theorem eqle

Description: Equality implies 'less than or equal to'. (Contributed by NM, 4-Apr-2005)

Ref Expression
Assertion eqle 
|- ( ( A e. RR /\ A = B ) -> A <_ B )

Proof

Step Hyp Ref Expression
1 leid 
 |-  ( A e. RR -> A <_ A )
2 breq2 
 |-  ( A = B -> ( A <_ A <-> A <_ B ) )
3 2 biimpac 
 |-  ( ( A <_ A /\ A = B ) -> A <_ B )
4 1 3 sylan 
 |-  ( ( A e. RR /\ A = B ) -> A <_ B )