Theorem ifeq2d 4509

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

Syntax hints:   → wi 4   = wceq 1540  ifcif 4488

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-un 3919  df-if 4489

This theorem is referenced by:  ifeq12d  4510  ifbieq2d  4515  ifeq2da  4521  ifcomnan  4545  rdgeq1  8379  cantnflem1d  9641  cantnflem1  9642  rexmul  13231  1arithlem4  16897  ramcl  17000  mplcoe1  21944  mplcoe5  21947  subrgascl  21973  selvffval  22020  selvval  22022  scmatscm  22400  marrepfval  22447  ma1repveval  22458  mulmarep1el  22459  mdetralt2  22496  mdetunilem8  22506  maduval  22525  maducoeval2  22527  madurid  22531  minmar1val0  22534  monmatcollpw  22666  pmatcollpwscmatlem1  22676  monmat2matmon  22711  itg2monolem1  25651  iblmulc2  25732  itgmulc2lem1  25733  bddmulibl  25740  dvtaylp  26278  dchrinvcl  27164  rpvmasum2  27423  padicfval  27527  expsval  28311  plymulx  34539  itg2addnclem  37665  itg2addnclem3  37667  itg2addnc  37668  itgmulc2nclem1  37680  hdmap1fval  41790  cantnfresb  43313  itgioocnicc  45975  etransclem14  46246  etransclem17  46249  etransclem21  46253  etransclem25  46257  etransclem28  46260  etransclem31  46263  hsphoif  46574  hoidmvval  46575  hsphoival  46577  hoidmvlelem5  46597  hoidmvle  46598  ovnhoi  46601  hspmbllem2  46625