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 ) )