Theorem ibllem

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

	Ref	Expression
Hypothesis	ibllem.1	$$⊢\left(\phi \wedge x\in A\right)\to B=C$$
Assertion	ibllem	$$⊢\phi \to if\left(\left(x\in A\wedge 0\le B\right),B,0\right)=if\left(\left(x\in A\wedge 0\le C\right),C,0\right)$$

Proof

Step	Hyp	Ref	Expression
1		ibllem.1	$$⊢\left(\phi \wedge x\in A\right)\to B=C$$
2	1	breq2d	$$⊢\left(\phi \wedge x\in A\right)\to \left(0\le B\leftrightarrow 0\le C\right)$$
3	2	pm5.32da	$$⊢\phi \to \left(\left(x\in A\wedge 0\le B\right)\leftrightarrow \left(x\in A\wedge 0\le C\right)\right)$$
4	3	ifbid	$$⊢\phi \to if\left(\left(x\in A\wedge 0\le B\right),B,0\right)=if\left(\left(x\in A\wedge 0\le C\right),B,0\right)$$
5	1	adantrr	$$⊢\left(\phi \wedge \left(x\in A\wedge 0\le C\right)\right)\to B=C$$
6	5	ifeq1da	$$⊢\phi \to if\left(\left(x\in A\wedge 0\le C\right),B,0\right)=if\left(\left(x\in A\wedge 0\le C\right),C,0\right)$$
7	4 6	eqtrd	$$⊢\phi \to if\left(\left(x\in A\wedge 0\le B\right),B,0\right)=if\left(\left(x\in A\wedge 0\le C\right),C,0\right)$$