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

Theorem ifeq2d 3953
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 3939 . 2  |-  ( A  =  B  ->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B ) )
31, 2syl 16 1  |-  ( ph  ->  if ( ps ,  C ,  A )  =  if ( ps ,  C ,  B )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1374   ifcif 3934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-rab 2818  df-v 3110  df-un 3476  df-if 3935
This theorem is referenced by:  ifeq12d  3954  ifbieq2d  3959  ifeq2da  3965  ifcomnan  3983  rdgeq1  7069  cantnflem1d  8098  cantnflem1  8099  cantnflem1dOLD  8121  cantnflem1OLD  8122  rexmul  11454  1arithlem4  14294  ramcl  14397  mplcoe1  17893  mplcoe5  17897  mplcoe2OLD  17899  subrgascl  17929  scmatscm  18777  marrepfval  18824  ma1repveval  18835  mulmarep1el  18836  mdetralt2  18873  mdetunilem8  18883  maduval  18902  maducoeval2  18904  madurid  18908  minmar1val0  18911  monmatcollpw  19042  pmatcollpwscmatlem1  19052  monmat2matmon  19087  itg2monolem1  21887  iblmulc2  21967  itgmulc2lem1  21968  bddmulibl  21975  dvtaylp  22494  dchrinvcl  23251  rpvmasum2  23420  padicfval  23524  gxval  24924  plymulx  28133  itg2addnclem  29632  itg2addnclem3  29634  itg2addnc  29635  itgmulc2nclem1  29647  itgioocnicc  31252  fourierdlem76  31440  fourierdlem89  31453  hdmap1fval  36471
  Copyright terms: Public domain W3C validator