This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 iftrue ⊢ ( 𝜑 → if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 )
2 iftrue ⊢ ( 𝜑 → if ( 𝜑 , 𝐶 , 𝐷 ) = 𝐶 )
3 1 2 oveq12d ⊢ ( 𝜑 → ( if ( 𝜑 , 𝐴 , 𝐵 ) 𝐹 if ( 𝜑 , 𝐶 , 𝐷 ) ) = ( 𝐴 𝐹 𝐶 ) )
4 iftrue ⊢ ( 𝜑 → if ( 𝜑 , ( 𝐴 𝐹 𝐶 ) , ( 𝐵 𝐹 𝐷 ) ) = ( 𝐴 𝐹 𝐶 ) )
5 3 4 eqtr4d ⊢ ( 𝜑 → ( if ( 𝜑 , 𝐴 , 𝐵 ) 𝐹 if ( 𝜑 , 𝐶 , 𝐷 ) ) = if ( 𝜑 , ( 𝐴 𝐹 𝐶 ) , ( 𝐵 𝐹 𝐷 ) ) )
6 iffalse ⊢ ( ¬ 𝜑 → if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐵 )
7 iffalse ⊢ ( ¬ 𝜑 → if ( 𝜑 , 𝐶 , 𝐷 ) = 𝐷 )
8 6 7 oveq12d ⊢ ( ¬ 𝜑 → ( if ( 𝜑 , 𝐴 , 𝐵 ) 𝐹 if ( 𝜑 , 𝐶 , 𝐷 ) ) = ( 𝐵 𝐹 𝐷 ) )
9 iffalse ⊢ ( ¬ 𝜑 → if ( 𝜑 , ( 𝐴 𝐹 𝐶 ) , ( 𝐵 𝐹 𝐷 ) ) = ( 𝐵 𝐹 𝐷 ) )
10 8 9 eqtr4d ⊢ ( ¬ 𝜑 → ( if ( 𝜑 , 𝐴 , 𝐵 ) 𝐹 if ( 𝜑 , 𝐶 , 𝐷 ) ) = if ( 𝜑 , ( 𝐴 𝐹 𝐶 ) , ( 𝐵 𝐹 𝐷 ) ) )
11 5 10 pm2.61i ⊢ ( if ( 𝜑 , 𝐴 , 𝐵 ) 𝐹 if ( 𝜑 , 𝐶 , 𝐷 ) ) = if ( 𝜑 , ( 𝐴 𝐹 𝐶 ) , ( 𝐵 𝐹 𝐷 ) )