Theorem ifov

Description: Move a conditional outside of an operation. (Contributed by AV, 11-Nov-2019)

	Ref	Expression
Assertion	ifov	$$⊢Aif\left(\phi ,F,G\right)B=if\left(\phi ,AFB,AGB\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq	$$⊢if\left(\phi ,F,G\right)=F\to Aif\left(\phi ,F,G\right)B=AFB$$
2		oveq	$$⊢if\left(\phi ,F,G\right)=G\to Aif\left(\phi ,F,G\right)B=AGB$$
3	1 2	ifsb	$$⊢Aif\left(\phi ,F,G\right)B=if\left(\phi ,AFB,AGB\right)$$