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 ( ph , A , B ) F if ( ph , C , D ) ) = if ( ph , ( A F C ) , ( B F D ) )

Proof

Step Hyp Ref Expression
1 iftrue
 |-  ( ph -> if ( ph , A , B ) = A )
2 iftrue
 |-  ( ph -> if ( ph , C , D ) = C )
3 1 2 oveq12d
 |-  ( ph -> ( if ( ph , A , B ) F if ( ph , C , D ) ) = ( A F C ) )
4 iftrue
 |-  ( ph -> if ( ph , ( A F C ) , ( B F D ) ) = ( A F C ) )
5 3 4 eqtr4d
 |-  ( ph -> ( if ( ph , A , B ) F if ( ph , C , D ) ) = if ( ph , ( A F C ) , ( B F D ) ) )
6 iffalse
 |-  ( -. ph -> if ( ph , A , B ) = B )
7 iffalse
 |-  ( -. ph -> if ( ph , C , D ) = D )
8 6 7 oveq12d
 |-  ( -. ph -> ( if ( ph , A , B ) F if ( ph , C , D ) ) = ( B F D ) )
9 iffalse
 |-  ( -. ph -> if ( ph , ( A F C ) , ( B F D ) ) = ( B F D ) )
10 8 9 eqtr4d
 |-  ( -. ph -> ( if ( ph , A , B ) F if ( ph , C , D ) ) = if ( ph , ( A F C ) , ( B F D ) ) )
11 5 10 pm2.61i
 |-  ( if ( ph , A , B ) F if ( ph , C , D ) ) = if ( ph , ( A F C ) , ( B F D ) )