Theorem ifeq2d 4479

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

Syntax hints:   → wi 4   = wceq 1539  ifcif 4459

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-un 3892  df-if 4460

This theorem is referenced by:  ifeq12d  4480  ifbieq2d  4485  ifeq2da  4491  ifcomnan  4515  rdgeq1  8242  cantnflem1d  9446  cantnflem1  9447  rexmul  13005  1arithlem4  16627  ramcl  16730  mplcoe1  21238  mplcoe5  21241  subrgascl  21274  selvffval  21326  selvval  21328  scmatscm  21662  marrepfval  21709  ma1repveval  21720  mulmarep1el  21721  mdetralt2  21758  mdetunilem8  21768  maduval  21787  maducoeval2  21789  madurid  21793  minmar1val0  21796  monmatcollpw  21928  pmatcollpwscmatlem1  21938  monmat2matmon  21973  itg2monolem1  24915  iblmulc2  24995  itgmulc2lem1  24996  bddmulibl  25003  dvtaylp  25529  dchrinvcl  26401  rpvmasum2  26660  padicfval  26764  plymulx  32527  itg2addnclem  35828  itg2addnclem3  35830  itg2addnc  35831  itgmulc2nclem1  35843  hdmap1fval  39810  itgioocnicc  43518  etransclem14  43789  etransclem17  43792  etransclem21  43796  etransclem25  43800  etransclem28  43803  etransclem31  43806  hsphoif  44114  hoidmvval  44115  hsphoival  44117  hoidmvlelem5  44137  hoidmvle  44138  ovnhoi  44141  hspmbllem2  44165