Theorem ifeq2d 4526

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

Syntax hints:   → wi 4   = wceq 1540  ifcif 4505

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-un 3936  df-if 4506

This theorem is referenced by:  ifeq12d  4527  ifbieq2d  4532  ifeq2da  4538  ifcomnan  4562  rdgeq1  8430  cantnflem1d  9707  cantnflem1  9708  rexmul  13292  1arithlem4  16951  ramcl  17054  mplcoe1  22000  mplcoe5  22003  subrgascl  22029  selvffval  22076  selvval  22078  scmatscm  22456  marrepfval  22503  ma1repveval  22514  mulmarep1el  22515  mdetralt2  22552  mdetunilem8  22562  maduval  22581  maducoeval2  22583  madurid  22587  minmar1val0  22590  monmatcollpw  22722  pmatcollpwscmatlem1  22732  monmat2matmon  22767  itg2monolem1  25708  iblmulc2  25789  itgmulc2lem1  25790  bddmulibl  25797  dvtaylp  26335  dchrinvcl  27221  rpvmasum2  27480  padicfval  27584  expsval  28368  plymulx  34585  itg2addnclem  37700  itg2addnclem3  37702  itg2addnc  37703  itgmulc2nclem1  37715  hdmap1fval  41820  cantnfresb  43323  itgioocnicc  45986  etransclem14  46257  etransclem17  46260  etransclem21  46264  etransclem25  46268  etransclem28  46271  etransclem31  46274  hsphoif  46585  hoidmvval  46586  hsphoival  46588  hoidmvlelem5  46608  hoidmvle  46609  ovnhoi  46612  hspmbllem2  46636