Theorem ifeq2d 4508

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

Syntax hints:   → wi 4   = wceq 1570  ifcif 4487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-un 3910  df-if 4488

This theorem is referenced by:  ifeq12d  4509  ifbieq2d  4514  ifeq2da  4520  ifcomnan  4544  rdgeq1  8394  cantnflem1d  9653  cantnflem1  9654  rexmul  13292  1arithlem4  16981  ramcl  17084  mplcoe1  22188  mplcoe5  22191  subrgascl  22217  selvffval  22269  selvval  22271  scmatscm  22670  marrepfval  22717  ma1repveval  22728  mulmarep1el  22729  mdetralt2  22766  mdetunilem8  22776  maduval  22795  maducoeval2  22797  madurid  22801  minmar1val0  22804  monmatcollpw  22936  pmatcollpwscmatlem1  22946  monmat2matmon  22981  itg2monolem1  25909  iblmulc2  25990  itgmulc2lem1  25991  bddmulibl  25998  plymulidp  26443  dvtaylp  26533  dchrinvcl  27417  rpvmasum2  27676  padicfval  27780  expsval  28618  itg2addnclem  38322  itg2addnclem3  38324  itg2addnc  38325  itgmulc2nclem1  38337  hdmap1fval  42570  cantnfresb  44051  itgioocnicc  46691  etransclem14  46962  etransclem17  46965  etransclem21  46969  etransclem25  46973  etransclem28  46976  etransclem31  46979  hsphoif  47290  hoidmvval  47291  hsphoival  47293  hoidmvlelem5  47313  hoidmvle  47314  ovnhoi  47317  hspmbllem2  47341