Metamath Proof Explorer

Theorem ovif2

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

Ref Expression
Assertion ovif2 ⊢ A F if φ B C = if φ A F B A F C

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ if φ B C = B → A F if φ B C = A F B
2 oveq2 ⊢ if φ B C = C → A F if φ B C = A F C
3 1 2 ifsb ⊢ A F if φ B C = if φ A F B A F C