Metamath Proof Explorer


Theorem leeq2d

Description: Specialization of breq2d to reals and less than. (Contributed by Stanislas Polu, 9-Mar-2020)

Ref Expression
Hypotheses leeq2d.1
|- ( ph -> A <_ C )
leeq2d.2
|- ( ph -> C = D )
leeq2d.3
|- ( ph -> A e. RR )
leeq2d.4
|- ( ph -> C e. RR )
Assertion leeq2d
|- ( ph -> A <_ D )

Proof

Step Hyp Ref Expression
1 leeq2d.1
 |-  ( ph -> A <_ C )
2 leeq2d.2
 |-  ( ph -> C = D )
3 leeq2d.3
 |-  ( ph -> A e. RR )
4 leeq2d.4
 |-  ( ph -> C e. RR )
5 1 2 breqtrd
 |-  ( ph -> A <_ D )