Theorem fvif

Description: Move a conditional outside of a function. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	fvif	$$⊢F\left(if\left(\phi ,A,B\right)\right)=if\left(\phi ,F\left(A\right),F\left(B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢if\left(\phi ,A,B\right)=A\to F\left(if\left(\phi ,A,B\right)\right)=F\left(A\right)$$
2		fveq2	$$⊢if\left(\phi ,A,B\right)=B\to F\left(if\left(\phi ,A,B\right)\right)=F\left(B\right)$$
3	1 2	ifsb	$$⊢F\left(if\left(\phi ,A,B\right)\right)=if\left(\phi ,F\left(A\right),F\left(B\right)\right)$$