Metamath Proof Explorer

Theorem ifle

Description: An if statement transforms an implication into an inequality of terms. (Contributed by Mario Carneiro, 31-Aug-2014)

Ref Expression
Assertion ifle ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≤ A ∧ φ → ψ → if φ A B ≤ if ψ A B

Proof

Step Hyp Ref Expression
1 simpll1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≤ A ∧ φ → ψ ∧ φ → A ∈ ℝ
2 1 leidd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≤ A ∧ φ → ψ ∧ φ → A ≤ A
3 iftrue ⊢ φ → if φ A B = A
4 3 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≤ A ∧ φ → ψ ∧ φ → if φ A B = A
5 id ⊢ φ → ψ → φ → ψ
6 5 imp ⊢ φ → ψ ∧ φ → ψ
7 6 adantll ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≤ A ∧ φ → ψ ∧ φ → ψ
8 7 iftrued ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≤ A ∧ φ → ψ ∧ φ → if ψ A B = A
9 2 4 8 3brtr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≤ A ∧ φ → ψ ∧ φ → if φ A B ≤ if ψ A B
10 iffalse ⊢ ¬ φ → if φ A B = B
11 10 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≤ A ∧ φ → ψ ∧ ¬ φ → if φ A B = B
12 simpll3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≤ A ∧ φ → ψ ∧ ¬ φ → B ≤ A
13 simpll2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≤ A ∧ φ → ψ ∧ ¬ φ → B ∈ ℝ
14 13 leidd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≤ A ∧ φ → ψ ∧ ¬ φ → B ≤ B
15 breq2 ⊢ A = if ψ A B → B ≤ A ↔ B ≤ if ψ A B
16 breq2 ⊢ B = if ψ A B → B ≤ B ↔ B ≤ if ψ A B
17 15 16 ifboth ⊢ B ≤ A ∧ B ≤ B → B ≤ if ψ A B
18 12 14 17 syl2anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≤ A ∧ φ → ψ ∧ ¬ φ → B ≤ if ψ A B
19 11 18 eqbrtrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≤ A ∧ φ → ψ ∧ ¬ φ → if φ A B ≤ if ψ A B
20 9 19 pm2.61dan ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ B ≤ A ∧ φ → ψ → if φ A B ≤ if ψ A B