Theorem ifeq2d 4549

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

Syntax hints:   → wi 4   = wceq 1542  ifcif 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-un 3954  df-if 4530

This theorem is referenced by:  ifeq12d  4550  ifbieq2d  4555  ifeq2da  4561  ifcomnan  4585  rdgeq1  8411  cantnflem1d  9683  cantnflem1  9684  rexmul  13250  1arithlem4  16859  ramcl  16962  mplcoe1  21592  mplcoe5  21595  subrgascl  21627  selvffval  21679  selvval  21681  scmatscm  22015  marrepfval  22062  ma1repveval  22073  mulmarep1el  22074  mdetralt2  22111  mdetunilem8  22121  maduval  22140  maducoeval2  22142  madurid  22146  minmar1val0  22149  monmatcollpw  22281  pmatcollpwscmatlem1  22291  monmat2matmon  22326  itg2monolem1  25268  iblmulc2  25348  itgmulc2lem1  25349  bddmulibl  25356  dvtaylp  25882  dchrinvcl  26756  rpvmasum2  27015  padicfval  27119  plymulx  33590  itg2addnclem  36587  itg2addnclem3  36589  itg2addnc  36590  itgmulc2nclem1  36602  hdmap1fval  40715  cantnfresb  42122  itgioocnicc  44741  etransclem14  45012  etransclem17  45015  etransclem21  45019  etransclem25  45023  etransclem28  45026  etransclem31  45029  hsphoif  45340  hoidmvval  45341  hsphoival  45343  hoidmvlelem5  45363  hoidmvle  45364  ovnhoi  45367  hspmbllem2  45391