Theorem ovif

Description: Move a conditional outside of an operation. (Contributed by Thierry Arnoux, 25-Jan-2017)

	Ref	Expression
Assertion	ovif	$$⊢if\left(\phi ,A,B\right)FC=if\left(\phi ,AFC,BFC\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢if\left(\phi ,A,B\right)=A\to if\left(\phi ,A,B\right)FC=AFC$$
2		oveq1	$$⊢if\left(\phi ,A,B\right)=B\to if\left(\phi ,A,B\right)FC=BFC$$
3	1 2	ifsb	$$⊢if\left(\phi ,A,B\right)FC=if\left(\phi ,AFC,BFC\right)$$