Theorem ifeq2d 4476

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

Syntax hints:   → wi 4   = wceq 1539  ifcif 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-un 3888  df-if 4457

This theorem is referenced by:  ifeq12d  4477  ifbieq2d  4482  ifeq2da  4488  ifcomnan  4512  rdgeq1  8213  cantnflem1d  9376  cantnflem1  9377  rexmul  12934  1arithlem4  16555  ramcl  16658  mplcoe1  21148  mplcoe5  21151  subrgascl  21184  selvffval  21236  selvval  21238  scmatscm  21570  marrepfval  21617  ma1repveval  21628  mulmarep1el  21629  mdetralt2  21666  mdetunilem8  21676  maduval  21695  maducoeval2  21697  madurid  21701  minmar1val0  21704  monmatcollpw  21836  pmatcollpwscmatlem1  21846  monmat2matmon  21881  itg2monolem1  24820  iblmulc2  24900  itgmulc2lem1  24901  bddmulibl  24908  dvtaylp  25434  dchrinvcl  26306  rpvmasum2  26565  padicfval  26669  plymulx  32427  itg2addnclem  35755  itg2addnclem3  35757  itg2addnc  35758  itgmulc2nclem1  35770  hdmap1fval  39737  itgioocnicc  43408  etransclem14  43679  etransclem17  43682  etransclem21  43686  etransclem25  43690  etransclem28  43693  etransclem31  43696  hsphoif  44004  hoidmvval  44005  hsphoival  44007  hoidmvlelem5  44027  hoidmvle  44028  ovnhoi  44031  hspmbllem2  44055