Theorem ifeq2d 4513

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

Syntax hints:   → wi 4   = wceq 1567  ifcif 4492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-un 3918  df-if 4493

This theorem is referenced by:  ifeq12d  4514  ifbieq2d  4519  ifeq2da  4525  ifcomnan  4549  rdgeq1  8397  cantnflem1d  9656  cantnflem1  9657  rexmul  13296  1arithlem4  16985  ramcl  17088  mplcoe1  22156  mplcoe5  22159  subrgascl  22185  selvffval  22237  selvval  22239  scmatscm  22638  marrepfval  22685  ma1repveval  22696  mulmarep1el  22697  mdetralt2  22734  mdetunilem8  22744  maduval  22763  maducoeval2  22765  madurid  22769  minmar1val0  22772  monmatcollpw  22904  pmatcollpwscmatlem1  22914  monmat2matmon  22949  itg2monolem1  25877  iblmulc2  25958  itgmulc2lem1  25959  bddmulibl  25966  plymulidp  26411  dvtaylp  26498  dchrinvcl  27382  rpvmasum2  27641  padicfval  27745  expsval  28583  itg2addnclem  38209  itg2addnclem3  38211  itg2addnc  38212  itgmulc2nclem1  38224  hdmap1fval  42459  cantnfresb  43942  itgioocnicc  46582  etransclem14  46853  etransclem17  46856  etransclem21  46860  etransclem25  46864  etransclem28  46867  etransclem31  46870  hsphoif  47181  hoidmvval  47182  hsphoival  47184  hoidmvlelem5  47204  hoidmvle  47205  ovnhoi  47208  hspmbllem2  47232