Theorem ifeq2d 4497

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

Syntax hints:   → wi 4   = wceq 1541  ifcif 4476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-un 3903  df-if 4477

This theorem is referenced by:  ifeq12d  4498  ifbieq2d  4503  ifeq2da  4509  ifcomnan  4533  rdgeq1  8339  cantnflem1d  9589  cantnflem1  9590  rexmul  13177  1arithlem4  16845  ramcl  16948  mplcoe1  21983  mplcoe5  21986  subrgascl  22012  selvffval  22067  selvval  22069  scmatscm  22448  marrepfval  22495  ma1repveval  22506  mulmarep1el  22507  mdetralt2  22544  mdetunilem8  22554  maduval  22573  maducoeval2  22575  madurid  22579  minmar1val0  22582  monmatcollpw  22714  pmatcollpwscmatlem1  22724  monmat2matmon  22759  itg2monolem1  25698  iblmulc2  25779  itgmulc2lem1  25780  bddmulibl  25787  dvtaylp  26325  dchrinvcl  27211  rpvmasum2  27470  padicfval  27574  expsval  28368  plymulx  34633  itg2addnclem  37784  itg2addnclem3  37786  itg2addnc  37787  itgmulc2nclem1  37799  hdmap1fval  41968  cantnfresb  43481  itgioocnicc  46137  etransclem14  46408  etransclem17  46411  etransclem21  46415  etransclem25  46419  etransclem28  46422  etransclem31  46425  hsphoif  46736  hoidmvval  46737  hsphoival  46739  hoidmvlelem5  46759  hoidmvle  46760  ovnhoi  46763  hspmbllem2  46787