Theorem ifeq2d 4488

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

Syntax hints:   → wi 4   = wceq 1542  ifcif 4467

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 3391  df-v 3432  df-un 3895  df-if 4468

This theorem is referenced by:  ifeq12d  4489  ifbieq2d  4494  ifeq2da  4500  ifcomnan  4524  rdgeq1  8343  cantnflem1d  9600  cantnflem1  9601  rexmul  13214  1arithlem4  16888  ramcl  16991  mplcoe1  22025  mplcoe5  22028  subrgascl  22054  selvffval  22109  selvval  22111  scmatscm  22488  marrepfval  22535  ma1repveval  22546  mulmarep1el  22547  mdetralt2  22584  mdetunilem8  22594  maduval  22613  maducoeval2  22615  madurid  22619  minmar1val0  22622  monmatcollpw  22754  pmatcollpwscmatlem1  22764  monmat2matmon  22799  itg2monolem1  25727  iblmulc2  25808  itgmulc2lem1  25809  bddmulibl  25816  dvtaylp  26347  dchrinvcl  27230  rpvmasum2  27489  padicfval  27593  expsval  28431  plymulx  34708  itg2addnclem  38006  itg2addnclem3  38008  itg2addnc  38009  itgmulc2nclem1  38021  hdmap1fval  42256  cantnfresb  43770  itgioocnicc  46423  etransclem14  46694  etransclem17  46697  etransclem21  46701  etransclem25  46705  etransclem28  46708  etransclem31  46711  hsphoif  47022  hoidmvval  47023  hsphoival  47025  hoidmvlelem5  47045  hoidmvle  47046  ovnhoi  47049  hspmbllem2  47073