Theorem ifeq2d 4545

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

Syntax hints:   → wi 4   = wceq 1539  ifcif 4524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-un 3955  df-if 4525

This theorem is referenced by:  ifeq12d  4546  ifbieq2d  4551  ifeq2da  4557  ifcomnan  4581  rdgeq1  8452  cantnflem1d  9729  cantnflem1  9730  rexmul  13314  1arithlem4  16965  ramcl  17068  mplcoe1  22056  mplcoe5  22059  subrgascl  22091  selvffval  22138  selvval  22140  scmatscm  22520  marrepfval  22567  ma1repveval  22578  mulmarep1el  22579  mdetralt2  22616  mdetunilem8  22626  maduval  22645  maducoeval2  22647  madurid  22651  minmar1val0  22654  monmatcollpw  22786  pmatcollpwscmatlem1  22796  monmat2matmon  22831  itg2monolem1  25786  iblmulc2  25867  itgmulc2lem1  25868  bddmulibl  25875  dvtaylp  26413  dchrinvcl  27298  rpvmasum2  27557  padicfval  27661  expsval  28409  plymulx  34564  itg2addnclem  37679  itg2addnclem3  37681  itg2addnc  37682  itgmulc2nclem1  37694  hdmap1fval  41799  cantnfresb  43342  itgioocnicc  45997  etransclem14  46268  etransclem17  46271  etransclem21  46275  etransclem25  46279  etransclem28  46282  etransclem31  46285  hsphoif  46596  hoidmvval  46597  hsphoival  46599  hoidmvlelem5  46619  hoidmvle  46620  ovnhoi  46623  hspmbllem2  46647