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 ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≤ 𝐴 ) ∧ ( 𝜑 → 𝜓 ) ) → if ( 𝜑 , 𝐴 , 𝐵 ) ≤ if ( 𝜓 , 𝐴 , 𝐵 ) )

Proof

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