Theorem ifeq2d 4477

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

Syntax hints:   → wi 4   = wceq 1548  ifcif 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-tru 1551  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-rab 3394  df-v 3435  df-un 3889  df-if 4457

This theorem is referenced by:  ifeq12d  4478  ifbieq2d  4483  ifeq2da  4489  ifcomnan  4513  rdgeq1  8344  cantnflem1d  9604  cantnflem1  9605  rexmul  13218  1arithlem4  16892  ramcl  16995  mplcoe1  22016  mplcoe5  22019  subrgascl  22045  selvffval  22097  selvval  22099  scmatscm  22499  marrepfval  22546  ma1repveval  22557  mulmarep1el  22558  mdetralt2  22595  mdetunilem8  22605  maduval  22624  maducoeval2  22626  madurid  22630  minmar1val0  22633  monmatcollpw  22765  pmatcollpwscmatlem1  22775  monmat2matmon  22810  itg2monolem1  25738  iblmulc2  25819  itgmulc2lem1  25820  bddmulibl  25827  dvtaylp  26356  dchrinvcl  27237  rpvmasum2  27496  padicfval  27600  expsval  28437  plymulx  34742  itg2addnclem  38051  itg2addnclem3  38053  itg2addnc  38054  itgmulc2nclem1  38066  hdmap1fval  42301  cantnfresb  43782  itgioocnicc  46432  etransclem14  46703  etransclem17  46706  etransclem21  46710  etransclem25  46714  etransclem28  46717  etransclem31  46720  hsphoif  47031  hoidmvval  47032  hsphoival  47034  hoidmvlelem5  47054  hoidmvle  47055  ovnhoi  47058  hspmbllem2  47082