Theorem ibllem

Description: Conditioned equality theorem for the if statement. (Contributed by Mario Carneiro, 31-Jul-2014)

	Ref	Expression
Hypothesis	ibllem.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 = 𝐶 )
Assertion	ibllem	⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) )

Proof

Step	Hyp	Ref	Expression
1		ibllem.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 = 𝐶 )
2	1	breq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 0 ≤ 𝐵 ↔ 0 ≤ 𝐶 ) )
3	2	pm5.32da	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) ) )
4	3	ifbid	⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐵 , 0 ) )
5	1	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) ) → 𝐵 = 𝐶 )
6	5	ifeq1da	⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐵 , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) )
7	4 6	eqtrd	⊢ ( 𝜑 → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐵 ) , 𝐵 , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ 𝐶 ) , 𝐶 , 0 ) )