Theorem iffv

Description: Move a conditional outside of a function. (Contributed by Thierry Arnoux, 28-Sep-2018)

	Ref	Expression
Assertion	iffv	|- ( if ( ph , F , G ) ` A ) = if ( ph , ( F ` A ) , ( G ` A ) )

Proof

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