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

Ref | Expression | ||
---|---|---|---|

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

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | oveq2 | ⊢ ( if ( 𝜑 , 𝐵 , 𝐶 ) = 𝐵 → ( 𝐴 𝐹 if ( 𝜑 , 𝐵 , 𝐶 ) ) = ( 𝐴 𝐹 𝐵 ) ) | |

2 | oveq2 | ⊢ ( if ( 𝜑 , 𝐵 , 𝐶 ) = 𝐶 → ( 𝐴 𝐹 if ( 𝜑 , 𝐵 , 𝐶 ) ) = ( 𝐴 𝐹 𝐶 ) ) | |

3 | 1 2 | ifsb | ⊢ ( 𝐴 𝐹 if ( 𝜑 , 𝐵 , 𝐶 ) ) = if ( 𝜑 , ( 𝐴 𝐹 𝐵 ) , ( 𝐴 𝐹 𝐶 ) ) |