Theorem ifeq2d 4551

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 4536	. 2 ⊢ (𝐴 = 𝐵 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → if(𝜓, 𝐶, 𝐴) = if(𝜓, 𝐶, 𝐵))

Syntax hints:   → wi 4   = wceq 1537  ifcif 4531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-un 3968  df-if 4532

This theorem is referenced by:  ifeq12d  4552  ifbieq2d  4557  ifeq2da  4563  ifcomnan  4587  rdgeq1  8450  cantnflem1d  9726  cantnflem1  9727  rexmul  13310  1arithlem4  16960  ramcl  17063  mplcoe1  22073  mplcoe5  22076  subrgascl  22108  selvffval  22155  selvval  22157  scmatscm  22535  marrepfval  22582  ma1repveval  22593  mulmarep1el  22594  mdetralt2  22631  mdetunilem8  22641  maduval  22660  maducoeval2  22662  madurid  22666  minmar1val0  22669  monmatcollpw  22801  pmatcollpwscmatlem1  22811  monmat2matmon  22846  itg2monolem1  25800  iblmulc2  25881  itgmulc2lem1  25882  bddmulibl  25889  dvtaylp  26427  dchrinvcl  27312  rpvmasum2  27571  padicfval  27675  expsval  28423  plymulx  34542  itg2addnclem  37658  itg2addnclem3  37660  itg2addnc  37661  itgmulc2nclem1  37673  hdmap1fval  41779  cantnfresb  43314  itgioocnicc  45933  etransclem14  46204  etransclem17  46207  etransclem21  46211  etransclem25  46215  etransclem28  46218  etransclem31  46221  hsphoif  46532  hoidmvval  46533  hsphoival  46535  hoidmvlelem5  46555  hoidmvle  46556  ovnhoi  46559  hspmbllem2  46583