Theorem ifeq2d 4506

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ifcif 4485

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-un 4154  df-if 4486

This theorem is used by:  ifeq12d  4507  ifbieq2d  4512  ifeq2da  4518  ifcomnan  4542  rdgeq1  8457  cantnflem1d  9726  cantnflem1  9727  rexmul  13441  1arithlem4  17148  ramcl  17251  mplcoe1  22401  mplcoe5  22404  subrgascl  22430  selvffval  22482  selvval  22484  scmatscm  22883  marrepfval  22930  ma1repveval  22941  mulmarep1el  22942  mdetralt2  22979  mdetunilem8  22989  maduval  23008  maducoeval2  23010  madurid  23014  minmar1val0  23017  monmatcollpw  23152  pmatcollpwscmatlem1  23162  monmat2matmon  23197  itg2monolem1  26126  iblmulc2  26206  itgmulc2lem1  26207  bddmulibl  26214  plymulidp  26658  dvtaylp  26754  dchrinvcl  27637  rpvmasum2  27896  padicfval  28000  expsval  28868  itg2addnclem  38857  itg2addnclem3  38859  itg2addnc  38860  itgmulc2nclem1  38872  hdmap1fval  43119  cantnfresb  44587  itgioocnicc  47260  etransclem14  47531  etransclem17  47534  etransclem21  47538  etransclem25  47542  etransclem28  47545  etransclem31  47548  hsphoif  47859  hoidmvval  47860  hsphoival  47862  hoidmvlelem5  47882  hoidmvle  47883  ovnhoi  47886  hspmbllem2  47910