Theorem fvif

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

	Ref	Expression
Assertion	fvif	|- ( F ` if ( ph , A , B ) ) = if ( ph , ( F ` A ) , ( F ` B ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	|- ( if ( ph , A , B ) = A -> ( F ` if ( ph , A , B ) ) = ( F ` A ) )
2		fveq2	|- ( if ( ph , A , B ) = B -> ( F ` if ( ph , A , B ) ) = ( F ` B ) )
3	1 2	ifsb	|- ( F ` if ( ph , A , B ) ) = if ( ph , ( F ` A ) , ( F ` B ) )