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