Theorem ifeq2d 4510

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-un 3911  df-if 4490

This theorem is used by:  ifeq12d  4511  ifbieq2d  4516  ifeq2da  4522  ifcomnan  4546  rdgeq1  8404  cantnflem1d  9664  cantnflem1  9665  rexmul  13313  1arithlem4  17008  ramcl  17111  mplcoe1  22238  mplcoe5  22241  subrgascl  22267  selvffval  22319  selvval  22321  scmatscm  22720  marrepfval  22767  ma1repveval  22778  mulmarep1el  22779  mdetralt2  22816  mdetunilem8  22826  maduval  22845  maducoeval2  22847  madurid  22851  minmar1val0  22854  monmatcollpw  22986  pmatcollpwscmatlem1  22996  monmat2matmon  23031  itg2monolem1  25960  iblmulc2  26041  itgmulc2lem1  26042  bddmulibl  26049  plymulidp  26494  dvtaylp  26584  dchrinvcl  27468  rpvmasum2  27727  padicfval  27831  expsval  28669  itg2addnclem  38379  itg2addnclem3  38381  itg2addnc  38382  itgmulc2nclem1  38394  hdmap1fval  42628  cantnfresb  44109  itgioocnicc  46749  etransclem14  47020  etransclem17  47023  etransclem21  47027  etransclem25  47031  etransclem28  47034  etransclem31  47037  hsphoif  47348  hoidmvval  47349  hsphoival  47351  hoidmvlelem5  47371  hoidmvle  47372  ovnhoi  47375  hspmbllem2  47399