Theorem ifeq2d 4475

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

Syntax hints:   → wi 4   = wceq 1547  ifcif 4454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-un 3888  df-if 4455

This theorem is referenced by:  ifeq12d  4476  ifbieq2d  4481  ifeq2da  4487  ifcomnan  4511  rdgeq1  8340  cantnflem1d  9600  cantnflem1  9601  rexmul  13214  1arithlem4  16888  ramcl  16991  mplcoe1  22013  mplcoe5  22016  subrgascl  22042  selvffval  22094  selvval  22096  scmatscm  22496  marrepfval  22543  ma1repveval  22554  mulmarep1el  22555  mdetralt2  22592  mdetunilem8  22602  maduval  22621  maducoeval2  22623  madurid  22627  minmar1val0  22630  monmatcollpw  22762  pmatcollpwscmatlem1  22772  monmat2matmon  22807  itg2monolem1  25735  iblmulc2  25816  itgmulc2lem1  25817  bddmulibl  25824  dvtaylp  26353  dchrinvcl  27234  rpvmasum2  27493  padicfval  27597  expsval  28435  plymulx  34732  itg2addnclem  38038  itg2addnclem3  38040  itg2addnc  38041  itgmulc2nclem1  38053  hdmap1fval  42288  cantnfresb  43769  itgioocnicc  46420  etransclem14  46691  etransclem17  46694  etransclem21  46698  etransclem25  46702  etransclem28  46705  etransclem31  46708  hsphoif  47019  hoidmvval  47020  hsphoival  47022  hoidmvlelem5  47042  hoidmvle  47043  ovnhoi  47046  hspmbllem2  47070