Metamath Proof Explorer


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 ( 𝜑 , ( 𝐴 𝐹 𝐵 ) , ( 𝐴 𝐹 𝐶 ) )