Theorem ifov

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

	Ref	Expression
Assertion	ifov	⊢ ( 𝐴 if ( 𝜑 , 𝐹 , 𝐺 ) 𝐵 ) = if ( 𝜑 , ( 𝐴 𝐹 𝐵 ) , ( 𝐴 𝐺 𝐵 ) )

Proof

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