MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifsb Unicode version

Theorem ifsb 3587
Description: Distribute a function over an if-clause. (Contributed by Mario Carneiro, 14-Aug-2013.)
Hypotheses
Ref Expression
ifsb.1  |-  ( if ( ph ,  A ,  B )  =  A  ->  C  =  D )
ifsb.2  |-  ( if ( ph ,  A ,  B )  =  B  ->  C  =  E )
Assertion
Ref Expression
ifsb  |-  C  =  if ( ph ,  D ,  E )

Proof of Theorem ifsb
StepHypRef Expression
1 iftrue 3584 . . . 4  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
2 ifsb.1 . . . 4  |-  ( if ( ph ,  A ,  B )  =  A  ->  C  =  D )
31, 2syl 15 . . 3  |-  ( ph  ->  C  =  D )
4 iftrue 3584 . . 3  |-  ( ph  ->  if ( ph ,  D ,  E )  =  D )
53, 4eqtr4d 2331 . 2  |-  ( ph  ->  C  =  if (
ph ,  D ,  E ) )
6 iffalse 3585 . . . 4  |-  ( -. 
ph  ->  if ( ph ,  A ,  B )  =  B )
7 ifsb.2 . . . 4  |-  ( if ( ph ,  A ,  B )  =  B  ->  C  =  E )
86, 7syl 15 . . 3  |-  ( -. 
ph  ->  C  =  E )
9 iffalse 3585 . . 3  |-  ( -. 
ph  ->  if ( ph ,  D ,  E )  =  E )
108, 9eqtr4d 2331 . 2  |-  ( -. 
ph  ->  C  =  if ( ph ,  D ,  E ) )
115, 10pm2.61i 156 1  |-  C  =  if ( ph ,  D ,  E )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1632   ifcif 3578
This theorem is referenced by:  fvif  5556  xmulneg1  10605  ramcl  13092  itg2const  19111  itg2monolem1  19121  iblmulc2  19201  itgmulc2lem1  19202  bddmulibl  19209  leibpi  20254  efrlim  20280  musumsum  20448  muinv  20449  dchrinvcl  20508  lgsneg  20574  lgsdilem  20577  dchrvmasumiflem2  20667  rpvmasum2  20677  padicabvcxp  20797  ovif  23166  itg2addnclem  25003  itgmulc2nclem1  25017
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-if 3579
  Copyright terms: Public domain W3C validator