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φAB≤ifψAB

Proof

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