Theorem ifeq2d 4503

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ifcif 4482

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-un 3904  df-if 4483

This theorem is used by:  ifeq12d  4504  ifbieq2d  4509  ifeq2da  4515  ifcomnan  4539  rdgeq1  8412  cantnflem1d  9682  cantnflem1  9683  rexmul  13394  1arithlem4  17097  ramcl  17200  mplcoe1  22339  mplcoe5  22342  subrgascl  22368  selvffval  22420  selvval  22422  scmatscm  22821  marrepfval  22868  ma1repveval  22879  mulmarep1el  22880  mdetralt2  22917  mdetunilem8  22927  maduval  22946  maducoeval2  22948  madurid  22952  minmar1val0  22955  monmatcollpw  23090  pmatcollpwscmatlem1  23100  monmat2matmon  23135  itg2monolem1  26064  iblmulc2  26144  itgmulc2lem1  26145  bddmulibl  26152  plymulidp  26596  dvtaylp  26690  dchrinvcl  27573  rpvmasum2  27832  padicfval  27936  expsval  28804  itg2addnclem  38569  itg2addnclem3  38571  itg2addnc  38572  itgmulc2nclem1  38584  hdmap1fval  42833  cantnfresb  44310  itgioocnicc  46956  etransclem14  47227  etransclem17  47230  etransclem21  47234  etransclem25  47238  etransclem28  47241  etransclem31  47244  hsphoif  47555  hoidmvval  47556  hsphoival  47558  hoidmvlelem5  47578  hoidmvle  47579  ovnhoi  47582  hspmbllem2  47606