Theorem ifeq1d 4502

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ifcif 4482

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-un 3904  df-if 4483

This theorem is used by:  ifeq12d  4504  ifbieq1d  4507  ifeq1da  4514  rabsnif  4684  fsuppmptif  9372  cantnflem1  9671  sumeq2w  15782  cbvsum  15785  cbvsumv  15786  sumeq2sdv  15793  isumless  15937  prodeq2sdv  16014  prodss  16037  subgmulg  19267  evlslem2  22298  selvval  22339  dmatcrng  22727  scmatscmiddistr  22733  scmatcrng  22746  marrepfval  22785  mdetr0  22830  mdetunilem8  22844  madufval  22862  madugsum  22868  minmar1fval  22871  matunitlindflem1  22904  decpmatid  22998  monmatcollpw  23007  pmatcollpwscmatlem1  23017  cnmpopc  25159  pcoval2  25247  pcopt  25253  itgz  26011  iblss2  26036  itgss  26042  itgcn  26075  plyeq0lem  26439  dgrcolem2  26503  plydivlem4  26529  leibpi  27182  chtublem  27450  sumdchr  27511  bposlem6  27528  lgsval  27540  dchrvmasumiflem2  27741  padicabvcxp  27871  mplasclco  34029  extvfv  34046  dfrdg3  36376  cbvsumdavw  36902  ftc1anclem2  38446  ftc1anclem5  38449  ftc1anclem7  38451  fsuppssindlem2  43441  fsuppssind  43442  mnringmulrvald  45068  hoidifhspval  47439  hoimbl  47462  veronesevald  50807