Theorem ifeq2d 4497

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

Syntax hints:   → wi 4   = wceq 1540  ifcif 4476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-un 3908  df-if 4477

This theorem is referenced by:  ifeq12d  4498  ifbieq2d  4503  ifeq2da  4509  ifcomnan  4533  rdgeq1  8333  cantnflem1d  9584  cantnflem1  9585  rexmul  13173  1arithlem4  16838  ramcl  16941  mplcoe1  21942  mplcoe5  21945  subrgascl  21971  selvffval  22018  selvval  22020  scmatscm  22398  marrepfval  22445  ma1repveval  22456  mulmarep1el  22457  mdetralt2  22494  mdetunilem8  22504  maduval  22523  maducoeval2  22525  madurid  22529  minmar1val0  22532  monmatcollpw  22664  pmatcollpwscmatlem1  22674  monmat2matmon  22709  itg2monolem1  25649  iblmulc2  25730  itgmulc2lem1  25731  bddmulibl  25738  dvtaylp  26276  dchrinvcl  27162  rpvmasum2  27421  padicfval  27525  expsval  28317  plymulx  34516  itg2addnclem  37651  itg2addnclem3  37653  itg2addnc  37654  itgmulc2nclem1  37666  hdmap1fval  41775  cantnfresb  43297  itgioocnicc  45958  etransclem14  46229  etransclem17  46232  etransclem21  46236  etransclem25  46240  etransclem28  46243  etransclem31  46246  hsphoif  46557  hoidmvval  46558  hsphoival  46560  hoidmvlelem5  46580  hoidmvle  46581  ovnhoi  46584  hspmbllem2  46608