Metamath Proof Explorer

Theorem icossico2d

Description: Condition for a closed-below, open-above interval to be a subset of a closed-below, open-above interval. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses icossico2d.1 ⊢ φ → B ∈ ℝ *
icossico2d.2 ⊢ φ → C ∈ ℝ *
icossico2d.3 ⊢ φ → B ≤ A
Assertion icossico2d ⊢ φ → A C ⊆ B C

Proof

Step Hyp Ref Expression
1 icossico2d.1 ⊢ φ → B ∈ ℝ *
2 icossico2d.2 ⊢ φ → C ∈ ℝ *
3 icossico2d.3 ⊢ φ → B ≤ A
4 2 xrleidd ⊢ φ → C ≤ C
5 icossico ⊢ B ∈ ℝ * ∧ C ∈ ℝ * ∧ B ≤ A ∧ C ≤ C → A C ⊆ B C
6 1 2 3 4 5 syl22anc ⊢ φ → A C ⊆ B C