Theorem ovif2

Description: Move a conditional outside of an operation. (Contributed by Thierry Arnoux, 1-Oct-2018)

	Ref	Expression
Assertion	ovif2	$$⊢AFif\left(\phi ,B,C\right)=if\left(\phi ,AFB,AFC\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢if\left(\phi ,B,C\right)=B\to AFif\left(\phi ,B,C\right)=AFB$$
2		oveq2	$$⊢if\left(\phi ,B,C\right)=C\to AFif\left(\phi ,B,C\right)=AFC$$
3	1 2	ifsb	$$⊢AFif\left(\phi ,B,C\right)=if\left(\phi ,AFB,AFC\right)$$