Theorem ifeq2d 4138

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

Syntax hints:   → wi 4   = wceq 1523  ifcif 4119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-un 3612  df-if 4120

This theorem is referenced by:  ifeq12d  4139  ifbieq2d  4144  ifeq2da  4150  ifcomnan  4170  rdgeq1  7552  cantnflem1d  8623  cantnflem1  8624  rexmul  12139  1arithlem4  15677  ramcl  15780  mplcoe1  19513  mplcoe5  19516  subrgascl  19546  scmatscm  20367  marrepfval  20414  ma1repveval  20425  mulmarep1el  20426  mdetralt2  20463  mdetunilem8  20473  maduval  20492  maducoeval2  20494  madurid  20498  minmar1val0  20501  monmatcollpw  20632  pmatcollpwscmatlem1  20642  monmat2matmon  20677  itg2monolem1  23562  iblmulc2  23642  itgmulc2lem1  23643  bddmulibl  23650  dvtaylp  24169  dchrinvcl  25023  rpvmasum2  25246  padicfval  25350  plymulx  30753  itg2addnclem  33591  itg2addnclem3  33593  itg2addnc  33594  itgmulc2nclem1  33606  hdmap1fval  37403  itgioocnicc  40511  etransclem14  40783  etransclem17  40786  etransclem21  40790  etransclem25  40794  etransclem28  40797  etransclem31  40800  hsphoif  41111  hoidmvval  41112  hsphoival  41114  hoidmvlelem5  41134  hoidmvle  41135  ovnhoi  41138  hspmbllem2  41162