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 )