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

Syntax hints:   → wi 4   = wceq 1538  ifcif 4425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-un 3886  df-if 4426

This theorem is referenced by:  ifeq12d  4445  ifbieq2d  4450  ifeq2da  4456  ifcomnan  4479  rdgeq1  8030  cantnflem1d  9135  cantnflem1  9136  rexmul  12652  1arithlem4  16252  ramcl  16355  mplcoe1  20705  mplcoe5  20708  subrgascl  20737  selvffval  20788  selvval  20790  scmatscm  21118  marrepfval  21165  ma1repveval  21176  mulmarep1el  21177  mdetralt2  21214  mdetunilem8  21224  maduval  21243  maducoeval2  21245  madurid  21249  minmar1val0  21252  monmatcollpw  21384  pmatcollpwscmatlem1  21394  monmat2matmon  21429  itg2monolem1  24354  iblmulc2  24434  itgmulc2lem1  24435  bddmulibl  24442  dvtaylp  24965  dchrinvcl  25837  rpvmasum2  26096  padicfval  26200  plymulx  31928  itg2addnclem  35108  itg2addnclem3  35110  itg2addnc  35111  itgmulc2nclem1  35123  hdmap1fval  39092  itgioocnicc  42619  etransclem14  42890  etransclem17  42893  etransclem21  42897  etransclem25  42901  etransclem28  42904  etransclem31  42907  hsphoif  43215  hoidmvval  43216  hsphoival  43218  hoidmvlelem5  43238  hoidmvle  43239  ovnhoi  43242  hspmbllem2  43266