Theorem ovif2

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

	Ref	Expression
Assertion	ovif2	⊢ ( 𝐴 𝐹 if ( 𝜑 , 𝐵 , 𝐶 ) ) = if ( 𝜑 , ( 𝐴 𝐹 𝐵 ) , ( 𝐴 𝐹 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( if ( 𝜑 , 𝐵 , 𝐶 ) = 𝐵 → ( 𝐴 𝐹 if ( 𝜑 , 𝐵 , 𝐶 ) ) = ( 𝐴 𝐹 𝐵 ) )
2		oveq2	⊢ ( if ( 𝜑 , 𝐵 , 𝐶 ) = 𝐶 → ( 𝐴 𝐹 if ( 𝜑 , 𝐵 , 𝐶 ) ) = ( 𝐴 𝐹 𝐶 ) )
3	1 2	ifsb	⊢ ( 𝐴 𝐹 if ( 𝜑 , 𝐵 , 𝐶 ) ) = if ( 𝜑 , ( 𝐴 𝐹 𝐵 ) , ( 𝐴 𝐹 𝐶 ) )