Theorem ifeq2d 4498

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

Syntax hints:   → wi 4   = wceq 1559  ifcif 4477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-un 3907  df-if 4478

This theorem is referenced by:  ifeq12d  4499  ifbieq2d  4504  ifeq2da  4510  ifcomnan  4534  rdgeq1  8376  cantnflem1d  9637  cantnflem1  9638  rexmul  13268  1arithlem4  16953  ramcl  17056  mplcoe1  22078  mplcoe5  22081  subrgascl  22107  selvffval  22159  selvval  22161  scmatscm  22561  marrepfval  22608  ma1repveval  22619  mulmarep1el  22620  mdetralt2  22657  mdetunilem8  22667  maduval  22686  maducoeval2  22688  madurid  22692  minmar1val0  22695  monmatcollpw  22827  pmatcollpwscmatlem1  22837  monmat2matmon  22872  itg2monolem1  25800  iblmulc2  25881  itgmulc2lem1  25882  bddmulibl  25889  plymulidp  26334  dvtaylp  26421  dchrinvcl  27305  rpvmasum2  27564  padicfval  27668  expsval  28506  itg2addnclem  38131  itg2addnclem3  38133  itg2addnc  38134  itgmulc2nclem1  38146  hdmap1fval  42381  cantnfresb  43862  itgioocnicc  46512  etransclem14  46783  etransclem17  46786  etransclem21  46790  etransclem25  46794  etransclem28  46797  etransclem31  46800  hsphoif  47111  hoidmvval  47112  hsphoival  47114  hoidmvlelem5  47134  hoidmvle  47135  ovnhoi  47138  hspmbllem2  47162