Theorem iffv

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

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

Proof

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