Theorem ifeq2d 4568

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

Syntax hints:   → wi 4   = wceq 1537  ifcif 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-un 3981  df-if 4549

This theorem is referenced by:  ifeq12d  4569  ifbieq2d  4574  ifeq2da  4580  ifcomnan  4604  rdgeq1  8467  cantnflem1d  9757  cantnflem1  9758  rexmul  13333  1arithlem4  16973  ramcl  17076  mplcoe1  22078  mplcoe5  22081  subrgascl  22113  selvffval  22160  selvval  22162  scmatscm  22540  marrepfval  22587  ma1repveval  22598  mulmarep1el  22599  mdetralt2  22636  mdetunilem8  22646  maduval  22665  maducoeval2  22667  madurid  22671  minmar1val0  22674  monmatcollpw  22806  pmatcollpwscmatlem1  22816  monmat2matmon  22851  itg2monolem1  25805  iblmulc2  25886  itgmulc2lem1  25887  bddmulibl  25894  dvtaylp  26430  dchrinvcl  27315  rpvmasum2  27574  padicfval  27678  expsval  28426  plymulx  34525  itg2addnclem  37631  itg2addnclem3  37633  itg2addnc  37634  itgmulc2nclem1  37646  hdmap1fval  41753  cantnfresb  43286  itgioocnicc  45898  etransclem14  46169  etransclem17  46172  etransclem21  46176  etransclem25  46180  etransclem28  46183  etransclem31  46186  hsphoif  46497  hoidmvval  46498  hsphoival  46500  hoidmvlelem5  46520  hoidmvle  46521  ovnhoi  46524  hspmbllem2  46548