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

Theorem ifeq2d 4504
Description: Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.)
Hypothesis
Ref Expression
ifeq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
ifeq2d (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))

Proof of Theorem ifeq2d
StepHypRef Expression
1 ifeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 ifeq2 4489 . 2 (𝐴 = 𝐵 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
31, 2syl 17 1 (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  ifcif 4484
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rab 3406  df-v 3445  df-un 3913  df-if 4485
This theorem is referenced by:  ifeq12d  4505  ifbieq2d  4510  ifeq2da  4516  ifcomnan  4540  rdgeq1  8349  cantnflem1d  9582  cantnflem1  9583  rexmul  13144  1arithlem4  16758  ramcl  16861  mplcoe1  21390  mplcoe5  21393  subrgascl  21426  selvffval  21478  selvval  21480  scmatscm  21814  marrepfval  21861  ma1repveval  21872  mulmarep1el  21873  mdetralt2  21910  mdetunilem8  21920  maduval  21939  maducoeval2  21941  madurid  21945  minmar1val0  21948  monmatcollpw  22080  pmatcollpwscmatlem1  22090  monmat2matmon  22125  itg2monolem1  25067  iblmulc2  25147  itgmulc2lem1  25148  bddmulibl  25155  dvtaylp  25681  dchrinvcl  26553  rpvmasum2  26812  padicfval  26916  plymulx  32972  itg2addnclem  36067  itg2addnclem3  36069  itg2addnc  36070  itgmulc2nclem1  36082  hdmap1fval  40197  cantnfresb  41565  itgioocnicc  44119  etransclem14  44390  etransclem17  44393  etransclem21  44397  etransclem25  44401  etransclem28  44404  etransclem31  44407  hsphoif  44718  hoidmvval  44719  hsphoival  44721  hoidmvlelem5  44741  hoidmvle  44742  ovnhoi  44745  hspmbllem2  44769
  Copyright terms: Public domain W3C validator