Theorem ifeq2d 4444

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

Syntax hints:   → wi 4   = wceq 1539  ifcif 4424

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-12 2176  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-rab 3080  df-v 3412  df-un 3866  df-if 4425

This theorem is referenced by:  ifeq12d  4445  ifbieq2d  4450  ifeq2da  4456  ifcomnan  4480  rdgeq1  8064  cantnflem1d  9198  cantnflem1  9199  rexmul  12719  1arithlem4  16332  ramcl  16435  mplcoe1  20812  mplcoe5  20815  subrgascl  20842  selvffval  20894  selvval  20896  scmatscm  21228  marrepfval  21275  ma1repveval  21286  mulmarep1el  21287  mdetralt2  21324  mdetunilem8  21334  maduval  21353  maducoeval2  21355  madurid  21359  minmar1val0  21362  monmatcollpw  21494  pmatcollpwscmatlem1  21504  monmat2matmon  21539  itg2monolem1  24465  iblmulc2  24545  itgmulc2lem1  24546  bddmulibl  24553  dvtaylp  25079  dchrinvcl  25951  rpvmasum2  26210  padicfval  26314  plymulx  32060  itg2addnclem  35424  itg2addnclem3  35426  itg2addnc  35427  itgmulc2nclem1  35439  hdmap1fval  39408  itgioocnicc  43031  etransclem14  43302  etransclem17  43305  etransclem21  43309  etransclem25  43313  etransclem28  43316  etransclem31  43319  hsphoif  43627  hoidmvval  43628  hsphoival  43630  hoidmvlelem5  43650  hoidmvle  43651  ovnhoi  43654  hspmbllem2  43678