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

Theorem ifsb 3750
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 3747 . . . 4  |-  ( ph  ->  if ( ph ,  A ,  B )  =  A )
2 ifsb.1 . . . 4  |-  ( if ( ph ,  A ,  B )  =  A  ->  C  =  D )
31, 2syl 16 . . 3  |-  ( ph  ->  C  =  D )
4 iftrue 3747 . . 3  |-  ( ph  ->  if ( ph ,  D ,  E )  =  D )
53, 4eqtr4d 2473 . 2  |-  ( ph  ->  C  =  if (
ph ,  D ,  E ) )
6 iffalse 3748 . . . 4  |-  ( -. 
ph  ->  if ( ph ,  A ,  B )  =  B )
7 ifsb.2 . . . 4  |-  ( if ( ph ,  A ,  B )  =  B  ->  C  =  E )
86, 7syl 16 . . 3  |-  ( -. 
ph  ->  C  =  E )
9 iffalse 3748 . . 3  |-  ( -. 
ph  ->  if ( ph ,  D ,  E )  =  E )
108, 9eqtr4d 2473 . 2  |-  ( -. 
ph  ->  C  =  if ( ph ,  D ,  E ) )
115, 10pm2.61i 159 1  |-  C  =  if ( ph ,  D ,  E )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1653   ifcif 3741
This theorem is referenced by:  fvif  5745  xmulneg1  10850  ramcl  13399  itg2const  19634  itg2monolem1  19644  iblmulc2  19724  itgmulc2lem1  19725  bddmulibl  19732  leibpi  20784  efrlim  20810  musumsum  20979  muinv  20980  dchrinvcl  21039  lgsneg  21105  lgsdilem  21108  dchrvmasumiflem2  21198  rpvmasum2  21208  padicabvcxp  21328  ovif  24005  itg2addnclem  26258  itgaddnclem2  26266  itgmulc2nclem1  26273  ftc1anclem6  26287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-if 3742
  Copyright terms: Public domain W3C validator