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 ( 𝜑𝐴𝐶 )
leeq2d.2 ( 𝜑𝐶 = 𝐷 )
leeq2d.3 ( 𝜑𝐴 ∈ ℝ )
leeq2d.4 ( 𝜑𝐶 ∈ ℝ )
Assertion leeq2d ( 𝜑𝐴𝐷 )

Proof

Step Hyp Ref Expression
1 leeq2d.1 ( 𝜑𝐴𝐶 )
2 leeq2d.2 ( 𝜑𝐶 = 𝐷 )
3 leeq2d.3 ( 𝜑𝐴 ∈ ℝ )
4 leeq2d.4 ( 𝜑𝐶 ∈ ℝ )
5 1 2 breqtrd ( 𝜑𝐴𝐷 )