Theorem ifeq1d 4487

Description: Equality deduction for conditional operator. (Contributed by NM, 16-Feb-2005.)

Hypothesis

Ref	Expression
ifeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
ifeq1d	⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))

Proof of Theorem ifeq1d

Step	Hyp	Ref	Expression
1		ifeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		ifeq1 4471	. 2 ⊢ (𝐴 = 𝐵 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))

Syntax hints:   → wi 4   = wceq 1542  ifcif 4467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-un 3895  df-if 4468

This theorem is referenced by:  ifeq12d  4489  ifbieq1d  4492  ifeq1da  4499  rabsnif  4668  fsuppmptif  9305  cantnflem1  9601  sumeq2w  15645  cbvsum  15648  cbvsumv  15649  sumeq2sdv  15656  isumless  15801  prodeq2sdv  15879  prodss  15903  subgmulg  19107  evlslem2  22067  selvval  22111  dmatcrng  22477  scmatscmiddistr  22483  scmatcrng  22496  marrepfval  22535  mdetr0  22580  mdetunilem8  22594  madufval  22612  madugsum  22618  minmar1fval  22621  decpmatid  22745  monmatcollpw  22754  pmatcollpwscmatlem1  22764  cnmpopc  24905  pcoval2  24993  pcopt  24999  itgz  25758  iblss2  25783  itgss  25789  itgcn  25822  plyeq0lem  26185  dgrcolem2  26249  plydivlem4  26273  leibpi  26919  chtublem  27188  sumdchr  27249  bposlem6  27266  lgsval  27278  dchrvmasumiflem2  27479  padicabvcxp  27609  extvfv  33692  dfrdg3  35992  cbvsumdavw  36477  matunitlindflem1  37951  ftc1anclem2  38029  ftc1anclem5  38032  ftc1anclem7  38034  fsuppssindlem2  43039  fsuppssind  43040  mnringmulrvald  44672  hoidifhspval  47054  hoimbl  47077