Theorem ovif

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

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

Proof

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