Theorem ifeq2d 4326

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

Syntax hints:   → wi 4   = wceq 1601  ifcif 4307

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rab 3099  df-v 3400  df-un 3797  df-if 4308

This theorem is referenced by:  ifeq12d  4327  ifbieq2d  4332  ifeq2da  4338  ifcomnan  4361  rdgeq1  7792  cantnflem1d  8884  cantnflem1  8885  rexmul  12417  1arithlem4  16038  ramcl  16141  mplcoe1  19866  mplcoe5  19869  subrgascl  19898  scmatscm  20728  marrepfval  20775  ma1repveval  20786  mulmarep1el  20787  mdetralt2  20824  mdetunilem8  20834  maduval  20853  maducoeval2  20855  madurid  20859  minmar1val0  20862  monmatcollpw  20995  pmatcollpwscmatlem1  21005  monmat2matmon  21040  itg2monolem1  23958  iblmulc2  24038  itgmulc2lem1  24039  bddmulibl  24046  dvtaylp  24565  dchrinvcl  25434  rpvmasum2  25657  padicfval  25761  plymulx  31229  itg2addnclem  34091  itg2addnclem3  34093  itg2addnc  34094  itgmulc2nclem1  34106  hdmap1fval  37955  itgioocnicc  41130  etransclem14  41402  etransclem17  41405  etransclem21  41409  etransclem25  41413  etransclem28  41416  etransclem31  41419  hsphoif  41727  hoidmvval  41728  hsphoival  41730  hoidmvlelem5  41750  hoidmvle  41751  ovnhoi  41754  hspmbllem2  41778