Theorem ifsb

Description: Distribute a function over an if-clause. (Contributed by Mario Carneiro, 14-Aug-2013)

	Ref	Expression
Hypotheses	ifsb.1	$$⊢if\left(\phi ,A,B\right)=A\to C=D$$
	ifsb.2	$$⊢if\left(\phi ,A,B\right)=B\to C=E$$
Assertion	ifsb	$$⊢C=if\left(\phi ,D,E\right)$$

Proof

Step	Hyp	Ref	Expression
1		ifsb.1	$$⊢if\left(\phi ,A,B\right)=A\to C=D$$
2		ifsb.2	$$⊢if\left(\phi ,A,B\right)=B\to C=E$$
3		iftrue	$$⊢\phi \to if\left(\phi ,A,B\right)=A$$
4	3 1	syl	$$⊢\phi \to C=D$$
5		iftrue	$$⊢\phi \to if\left(\phi ,D,E\right)=D$$
6	4 5	eqtr4d	$$⊢\phi \to C=if\left(\phi ,D,E\right)$$
7		iffalse	$$⊢\neg \phi \to if\left(\phi ,A,B\right)=B$$
8	7 2	syl	$$⊢\neg \phi \to C=E$$
9		iffalse	$$⊢\neg \phi \to if\left(\phi ,D,E\right)=E$$
10	8 9	eqtr4d	$$⊢\neg \phi \to C=if\left(\phi ,D,E\right)$$
11	6 10	pm2.61i	$$⊢C=if\left(\phi ,D,E\right)$$