Theorem ifeq2d 4491

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

Syntax hints:   → wi 4   = wceq 1541  ifcif 4470

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-un 3902  df-if 4471

This theorem is referenced by:  ifeq12d  4492  ifbieq2d  4497  ifeq2da  4503  ifcomnan  4527  rdgeq1  8325  cantnflem1d  9573  cantnflem1  9574  rexmul  13165  1arithlem4  16833  ramcl  16936  mplcoe1  21967  mplcoe5  21970  subrgascl  21996  selvffval  22043  selvval  22045  scmatscm  22423  marrepfval  22470  ma1repveval  22481  mulmarep1el  22482  mdetralt2  22519  mdetunilem8  22529  maduval  22548  maducoeval2  22550  madurid  22554  minmar1val0  22557  monmatcollpw  22689  pmatcollpwscmatlem1  22699  monmat2matmon  22734  itg2monolem1  25673  iblmulc2  25754  itgmulc2lem1  25755  bddmulibl  25762  dvtaylp  26300  dchrinvcl  27186  rpvmasum2  27445  padicfval  27549  expsval  28343  plymulx  34553  itg2addnclem  37711  itg2addnclem3  37713  itg2addnc  37714  itgmulc2nclem1  37726  hdmap1fval  41835  cantnfresb  43357  itgioocnicc  46015  etransclem14  46286  etransclem17  46289  etransclem21  46293  etransclem25  46297  etransclem28  46300  etransclem31  46303  hsphoif  46614  hoidmvval  46615  hsphoival  46617  hoidmvlelem5  46637  hoidmvle  46638  ovnhoi  46641  hspmbllem2  46665