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

Metamath Proof Explorer

Theorem ifsb

Description: Distribute a function over an if-clause. (Contributed by Mario Carneiro, 14-Aug-2013)

Ref Expression
Hypotheses ifsb.1 
|- ( if ( ph , A , B ) = A -> C = D )
ifsb.2 
|- ( if ( ph , A , B ) = B -> C = E )
Assertion ifsb 
|- C = if ( ph , D , E )

Proof

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