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

Theorem ifeq2d 4507
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 4492 . 2 (𝐴 = 𝐵 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
31, 2syl 17 1 (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  ifcif 4487
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3407  df-v 3446  df-un 3916  df-if 4488
This theorem is referenced by:  ifeq12d  4508  ifbieq2d  4513  ifeq2da  4519  ifcomnan  4543  rdgeq1  8358  cantnflem1d  9629  cantnflem1  9630  rexmul  13196  1arithlem4  16803  ramcl  16906  mplcoe1  21454  mplcoe5  21457  subrgascl  21490  selvffval  21542  selvval  21544  scmatscm  21878  marrepfval  21925  ma1repveval  21936  mulmarep1el  21937  mdetralt2  21974  mdetunilem8  21984  maduval  22003  maducoeval2  22005  madurid  22009  minmar1val0  22012  monmatcollpw  22144  pmatcollpwscmatlem1  22154  monmat2matmon  22189  itg2monolem1  25131  iblmulc2  25211  itgmulc2lem1  25212  bddmulibl  25219  dvtaylp  25745  dchrinvcl  26617  rpvmasum2  26876  padicfval  26980  plymulx  33217  itg2addnclem  36175  itg2addnclem3  36177  itg2addnc  36178  itgmulc2nclem1  36190  hdmap1fval  40305  cantnfresb  41702  itgioocnicc  44304  etransclem14  44575  etransclem17  44578  etransclem21  44582  etransclem25  44586  etransclem28  44589  etransclem31  44592  hsphoif  44903  hoidmvval  44904  hsphoival  44906  hoidmvlelem5  44926  hoidmvle  44927  ovnhoi  44930  hspmbllem2  44954
  Copyright terms: Public domain W3C validator