Theorem ifeq2d 4487

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

Syntax hints:   → wi 4   = wceq 1542  ifcif 4466

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-un 3894  df-if 4467

This theorem is referenced by:  ifeq12d  4488  ifbieq2d  4493  ifeq2da  4499  ifcomnan  4523  rdgeq1  8350  cantnflem1d  9609  cantnflem1  9610  rexmul  13223  1arithlem4  16897  ramcl  17000  mplcoe1  22015  mplcoe5  22018  subrgascl  22044  selvffval  22099  selvval  22101  scmatscm  22478  marrepfval  22525  ma1repveval  22536  mulmarep1el  22537  mdetralt2  22574  mdetunilem8  22584  maduval  22603  maducoeval2  22605  madurid  22609  minmar1val0  22612  monmatcollpw  22744  pmatcollpwscmatlem1  22754  monmat2matmon  22789  itg2monolem1  25717  iblmulc2  25798  itgmulc2lem1  25799  bddmulibl  25806  dvtaylp  26335  dchrinvcl  27216  rpvmasum2  27475  padicfval  27579  expsval  28417  plymulx  34692  itg2addnclem  37992  itg2addnclem3  37994  itg2addnc  37995  itgmulc2nclem1  38007  hdmap1fval  42242  cantnfresb  43752  itgioocnicc  46405  etransclem14  46676  etransclem17  46679  etransclem21  46683  etransclem25  46687  etransclem28  46690  etransclem31  46693  hsphoif  47004  hoidmvval  47005  hsphoival  47007  hoidmvlelem5  47027  hoidmvle  47028  ovnhoi  47031  hspmbllem2  47055