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

Theorem ifeq2d 3593
Description: Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.)
Hypothesis
Ref Expression
ifeq1d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
ifeq2d  |-  ( ph  ->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B )
)

Proof of Theorem ifeq2d
StepHypRef Expression
1 ifeq1d.1 . 2  |-  ( ph  ->  A  =  B )
2 ifeq2 3583 . 2  |-  ( A  =  B  ->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B ) )
31, 2syl 15 1  |-  ( ph  ->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   ifcif 3578
This theorem is referenced by:  ifeq12d  3594  ifbieq2d  3598  ifeq2da  3604  rdgeq1  6440  cantnflem1d  7406  cantnflem1  7407  rexmul  10607  1arithlem4  12989  ramcl  13092  mplcoe1  16225  mplcoe2  16227  subrgascl  16255  itg2monolem1  19121  iblmulc2  19201  itgmulc2lem1  19202  bddmulibl  19209  dvtaylp  19765  dchrinvcl  20508  rpvmasum2  20677  padicfval  20781  gxval  20941  itgmulc2nclem1  25017  prodeq3ii  25411  hdmap1fval  32609
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-nfc 2421  df-rab 2565  df-v 2803  df-un 3170  df-if 3579
  Copyright terms: Public domain W3C validator