Metamath Proof Explorer

Theorem xreqled

Description: Equality implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses xreqled.1 
|- ( ph -> A e. RR* )
xreqled.2 
|- ( ph -> A = B )
Assertion xreqled 
|- ( ph -> A <_ B )

Proof

Step Hyp Ref Expression
1 xreqled.1 
 |-  ( ph -> A e. RR* )
2 xreqled.2 
 |-  ( ph -> A = B )
3 xreqle 
 |-  ( ( A e. RR* /\ A = B ) -> A <_ B )
4 1 2 3 syl2anc 
 |-  ( ph -> A <_ B )