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

Theorem ifsb 3952
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 3945 . . . 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 3945 . . 3  |-  ( ph  ->  if ( ph ,  D ,  E )  =  D )
53, 4eqtr4d 2511 . 2  |-  ( ph  ->  C  =  if (
ph ,  D ,  E ) )
6 iffalse 3948 . . . 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 3948 . . 3  |-  ( -. 
ph  ->  if ( ph ,  D ,  E )  =  E )
108, 9eqtr4d 2511 . 2  |-  ( -. 
ph  ->  C  =  if ( ph ,  D ,  E ) )
115, 10pm2.61i 164 1  |-  C  =  if ( ph ,  D ,  E )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1379   ifcif 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-if 3940
This theorem is referenced by:  fvif  5875  iffv  5876  ovif  6361  ovif2  6362  ifov  6364  xmulneg1  11457  ramcl  14399  matsc  18716  maducoeval2  18906  madugsum  18909  itg2const  21879  itg2monolem1  21889  iblmulc2  21969  itgmulc2lem1  21970  bddmulibl  21977  leibpi  22998  efrlim  23024  musumsum  23193  muinv  23194  dchrinvcl  23253  lgsneg  23319  lgsdilem  23322  dchrvmasumiflem2  23412  rpvmasum2  23422  padicabvcxp  23542  itgaddnclem2  29649  itgmulc2nclem1  29656  ftc1anclem6  29670
  Copyright terms: Public domain W3C validator