Theorem ifeq2d 4505

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

Syntax hints:   → wi 4   = wceq 1540  ifcif 4484

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 3403  df-v 3446  df-un 3916  df-if 4485

This theorem is referenced by:  ifeq12d  4506  ifbieq2d  4511  ifeq2da  4517  ifcomnan  4541  rdgeq1  8356  cantnflem1d  9617  cantnflem1  9618  rexmul  13207  1arithlem4  16873  ramcl  16976  mplcoe1  21920  mplcoe5  21923  subrgascl  21949  selvffval  21996  selvval  21998  scmatscm  22376  marrepfval  22423  ma1repveval  22434  mulmarep1el  22435  mdetralt2  22472  mdetunilem8  22482  maduval  22501  maducoeval2  22503  madurid  22507  minmar1val0  22510  monmatcollpw  22642  pmatcollpwscmatlem1  22652  monmat2matmon  22687  itg2monolem1  25627  iblmulc2  25708  itgmulc2lem1  25709  bddmulibl  25716  dvtaylp  26254  dchrinvcl  27140  rpvmasum2  27399  padicfval  27503  expsval  28287  plymulx  34512  itg2addnclem  37638  itg2addnclem3  37640  itg2addnc  37641  itgmulc2nclem1  37653  hdmap1fval  41763  cantnfresb  43286  itgioocnicc  45948  etransclem14  46219  etransclem17  46222  etransclem21  46226  etransclem25  46230  etransclem28  46233  etransclem31  46236  hsphoif  46547  hoidmvval  46548  hsphoival  46550  hoidmvlelem5  46570  hoidmvle  46571  ovnhoi  46574  hspmbllem2  46598