Metamath Proof Explorer

Theorem ovif12

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

Ref Expression
Assertion ovif12 ⊢ if φ A B F if φ C D = if φ A F C B F D

Proof

Step Hyp Ref Expression
1 iftrue ⊢ φ → if φ A B = A
2 iftrue ⊢ φ → if φ C D = C
3 1 2 oveq12d ⊢ φ → if φ A B F if φ C D = A F C
4 iftrue ⊢ φ → if φ A F C B F D = A F C
5 3 4 eqtr4d ⊢ φ → if φ A B F if φ C D = if φ A F C B F D
6 iffalse ⊢ ¬ φ → if φ A B = B
7 iffalse ⊢ ¬ φ → if φ C D = D
8 6 7 oveq12d ⊢ ¬ φ → if φ A B F if φ C D = B F D
9 iffalse ⊢ ¬ φ → if φ A F C B F D = B F D
10 8 9 eqtr4d ⊢ ¬ φ → if φ A B F if φ C D = if φ A F C B F D
11 5 10 pm2.61i ⊢ if φ A B F if φ C D = if φ A F C B F D