Theorem ifeq2d 4511

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

Syntax hints:   → wi 4   = wceq 1540  ifcif 4490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-un 3921  df-if 4491

This theorem is referenced by:  ifeq12d  4512  ifbieq2d  4517  ifeq2da  4523  ifcomnan  4547  rdgeq1  8381  cantnflem1d  9647  cantnflem1  9648  rexmul  13237  1arithlem4  16903  ramcl  17006  mplcoe1  21950  mplcoe5  21953  subrgascl  21979  selvffval  22026  selvval  22028  scmatscm  22406  marrepfval  22453  ma1repveval  22464  mulmarep1el  22465  mdetralt2  22502  mdetunilem8  22512  maduval  22531  maducoeval2  22533  madurid  22537  minmar1val0  22540  monmatcollpw  22672  pmatcollpwscmatlem1  22682  monmat2matmon  22717  itg2monolem1  25657  iblmulc2  25738  itgmulc2lem1  25739  bddmulibl  25746  dvtaylp  26284  dchrinvcl  27170  rpvmasum2  27429  padicfval  27533  expsval  28317  plymulx  34545  itg2addnclem  37660  itg2addnclem3  37662  itg2addnc  37663  itgmulc2nclem1  37675  hdmap1fval  41785  cantnfresb  43306  itgioocnicc  45968  etransclem14  46239  etransclem17  46242  etransclem21  46246  etransclem25  46250  etransclem28  46253  etransclem31  46256  hsphoif  46567  hoidmvval  46568  hsphoival  46570  hoidmvlelem5  46590  hoidmvle  46591  ovnhoi  46594  hspmbllem2  46618