Theorem ifsb

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

	Ref	Expression
Hypotheses	ifsb.1	|- ( if ( ph , A , B ) = A -> C = D )
	ifsb.2	|- ( if ( ph , A , B ) = B -> C = E )
Assertion	ifsb	|- C = if ( ph , D , E )

Proof

Step	Hyp	Ref	Expression
1		ifsb.1	|- ( if ( ph , A , B ) = A -> C = D )
2		ifsb.2	|- ( if ( ph , A , B ) = B -> C = E )
3		iftrue	|- ( ph -> if ( ph , A , B ) = A )
4	3 1	syl	|- ( ph -> C = D )
5		iftrue	|- ( ph -> if ( ph , D , E ) = D )
6	4 5	eqtr4d	|- ( ph -> C = if ( ph , D , E ) )
7		iffalse	|- ( -. ph -> if ( ph , A , B ) = B )
8	7 2	syl	|- ( -. ph -> C = E )
9		iffalse	|- ( -. ph -> if ( ph , D , E ) = E )
10	8 9	eqtr4d	|- ( -. ph -> C = if ( ph , D , E ) )
11	6 10	pm2.61i	|- C = if ( ph , D , E )