Theorem ifeq2d 4500

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

Step	Hyp	Ref	Expression
1		ifeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		ifeq2 4484	. 2 ⊢ (𝐴 = 𝐵 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))

Syntax hints:   → wi 4   = wceq 1541  ifcif 4479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-un 3906  df-if 4480

This theorem is referenced by:  ifeq12d  4501  ifbieq2d  4506  ifeq2da  4512  ifcomnan  4536  rdgeq1  8342  cantnflem1d  9597  cantnflem1  9598  rexmul  13186  1arithlem4  16854  ramcl  16957  mplcoe1  21992  mplcoe5  21995  subrgascl  22021  selvffval  22076  selvval  22078  scmatscm  22457  marrepfval  22504  ma1repveval  22515  mulmarep1el  22516  mdetralt2  22553  mdetunilem8  22563  maduval  22582  maducoeval2  22584  madurid  22588  minmar1val0  22591  monmatcollpw  22723  pmatcollpwscmatlem1  22733  monmat2matmon  22768  itg2monolem1  25707  iblmulc2  25788  itgmulc2lem1  25789  bddmulibl  25796  dvtaylp  26334  dchrinvcl  27220  rpvmasum2  27479  padicfval  27583  expsval  28421  plymulx  34705  itg2addnclem  37872  itg2addnclem3  37874  itg2addnc  37875  itgmulc2nclem1  37887  hdmap1fval  42056  cantnfresb  43566  itgioocnicc  46221  etransclem14  46492  etransclem17  46495  etransclem21  46499  etransclem25  46503  etransclem28  46506  etransclem31  46509  hsphoif  46820  hoidmvval  46821  hsphoival  46823  hoidmvlelem5  46843  hoidmvle  46844  ovnhoi  46847  hspmbllem2  46871