Theorem ifeq2d 4550

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

Syntax hints:   → wi 4   = wceq 1533  ifcif 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-un 3949  df-if 4531

This theorem is referenced by:  ifeq12d  4551  ifbieq2d  4556  ifeq2da  4562  ifcomnan  4586  rdgeq1  8432  cantnflem1d  9713  cantnflem1  9714  rexmul  13285  1arithlem4  16898  ramcl  17001  mplcoe1  21997  mplcoe5  22000  subrgascl  22032  selvffval  22081  selvval  22083  scmatscm  22459  marrepfval  22506  ma1repveval  22517  mulmarep1el  22518  mdetralt2  22555  mdetunilem8  22565  maduval  22584  maducoeval2  22586  madurid  22590  minmar1val0  22593  monmatcollpw  22725  pmatcollpwscmatlem1  22735  monmat2matmon  22770  itg2monolem1  25724  iblmulc2  25804  itgmulc2lem1  25805  bddmulibl  25812  dvtaylp  26350  dchrinvcl  27231  rpvmasum2  27490  padicfval  27594  plymulx  34311  itg2addnclem  37275  itg2addnclem3  37277  itg2addnc  37278  itgmulc2nclem1  37290  hdmap1fval  41399  cantnfresb  42895  itgioocnicc  45503  etransclem14  45774  etransclem17  45777  etransclem21  45781  etransclem25  45785  etransclem28  45788  etransclem31  45791  hsphoif  46102  hoidmvval  46103  hsphoival  46105  hoidmvlelem5  46125  hoidmvle  46126  ovnhoi  46129  hspmbllem2  46153