Theorem ifeq2d 4502

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-un 4150  df-if 4482

This theorem is used by:  ifeq12d  4503  ifbieq2d  4508  ifeq2da  4514  ifcomnan  4538  rdgeq1  8426  cantnflem1d  9696  cantnflem1  9697  rexmul  13408  1arithlem4  17113  ramcl  17216  mplcoe1  22355  mplcoe5  22358  subrgascl  22384  selvffval  22436  selvval  22438  scmatscm  22837  marrepfval  22884  ma1repveval  22895  mulmarep1el  22896  mdetralt2  22933  mdetunilem8  22943  maduval  22962  maducoeval2  22964  madurid  22968  minmar1val0  22971  monmatcollpw  23106  pmatcollpwscmatlem1  23116  monmat2matmon  23151  itg2monolem1  26080  iblmulc2  26160  itgmulc2lem1  26161  bddmulibl  26168  plymulidp  26612  dvtaylp  26706  dchrinvcl  27589  rpvmasum2  27848  padicfval  27952  expsval  28820  itg2addnclem  38698  itg2addnclem3  38700  itg2addnc  38701  itgmulc2nclem1  38713  hdmap1fval  42962  cantnfresb  44435  itgioocnicc  47095  etransclem14  47366  etransclem17  47369  etransclem21  47373  etransclem25  47377  etransclem28  47380  etransclem31  47383  hsphoif  47694  hoidmvval  47695  hsphoival  47697  hoidmvlelem5  47717  hoidmvle  47718  ovnhoi  47721  hspmbllem2  47745