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 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-un 3904  df-if 4483

This theorem is used by:  ifeq12d  4504  ifbieq2d  4509  ifeq2da  4515  ifcomnan  4539  rdgeq1  8400  cantnflem1d  9667  cantnflem1  9668  rexmul  13323  1arithlem4  17018  ramcl  17121  mplcoe1  22253  mplcoe5  22256  subrgascl  22282  selvffval  22334  selvval  22336  scmatscm  22735  marrepfval  22782  ma1repveval  22793  mulmarep1el  22794  mdetralt2  22831  mdetunilem8  22841  maduval  22860  maducoeval2  22862  madurid  22866  minmar1val0  22869  monmatcollpw  23004  pmatcollpwscmatlem1  23014  monmat2matmon  23049  itg2monolem1  25978  iblmulc2  26058  itgmulc2lem1  26059  bddmulibl  26066  plymulidp  26512  dvtaylp  26606  dchrinvcl  27489  rpvmasum2  27748  padicfval  27852  expsval  28690  itg2addnclem  38420  itg2addnclem3  38422  itg2addnc  38423  itgmulc2nclem1  38435  hdmap1fval  42669  cantnfresb  44165  itgioocnicc  46805  etransclem14  47076  etransclem17  47079  etransclem21  47083  etransclem25  47087  etransclem28  47090  etransclem31  47093  hsphoif  47404  hoidmvval  47405  hsphoival  47407  hoidmvlelem5  47427  hoidmvle  47428  ovnhoi  47431  hspmbllem2  47455