Theorem ifeq2d 4502

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

Syntax hints:   → wi 4   = wceq 1542  ifcif 4481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-un 3908  df-if 4482

This theorem is referenced by:  ifeq12d  4503  ifbieq2d  4508  ifeq2da  4514  ifcomnan  4538  rdgeq1  8352  cantnflem1d  9609  cantnflem1  9610  rexmul  13198  1arithlem4  16866  ramcl  16969  mplcoe1  22004  mplcoe5  22007  subrgascl  22033  selvffval  22088  selvval  22090  scmatscm  22469  marrepfval  22516  ma1repveval  22527  mulmarep1el  22528  mdetralt2  22565  mdetunilem8  22575  maduval  22594  maducoeval2  22596  madurid  22600  minmar1val0  22603  monmatcollpw  22735  pmatcollpwscmatlem1  22745  monmat2matmon  22780  itg2monolem1  25719  iblmulc2  25800  itgmulc2lem1  25801  bddmulibl  25808  dvtaylp  26346  dchrinvcl  27232  rpvmasum2  27491  padicfval  27595  expsval  28433  plymulx  34726  itg2addnclem  37922  itg2addnclem3  37924  itg2addnc  37925  itgmulc2nclem1  37937  hdmap1fval  42172  cantnfresb  43681  itgioocnicc  46335  etransclem14  46606  etransclem17  46609  etransclem21  46613  etransclem25  46617  etransclem28  46620  etransclem31  46623  hsphoif  46934  hoidmvval  46935  hsphoival  46937  hoidmvlelem5  46957  hoidmvle  46958  ovnhoi  46961  hspmbllem2  46985