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 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-un 3904  df-if 4483

This theorem is used by:  ifeq12d  4504  ifbieq1d  4507  ifeq1da  4514  rabsnif  4684  fsuppmptif  9384  cantnflem1  9683  sumeq2w  15852  cbvsum  15855  cbvsumv  15856  sumeq2sdv  15863  isumless  16007  prodeq2sdv  16084  prodss  16107  subgmulg  19344  evlslem2  22381  selvval  22422  dmatcrng  22810  scmatscmiddistr  22816  scmatcrng  22829  marrepfval  22868  mdetr0  22913  mdetunilem8  22927  madufval  22945  madugsum  22951  minmar1fval  22954  matunitlindflem1  22987  decpmatid  23081  monmatcollpw  23090  pmatcollpwscmatlem1  23100  cnmpopc  25242  pcoval2  25330  pcopt  25336  itgz  26094  iblss2  26119  itgss  26125  itgcn  26158  plyeq0lem  26522  dgrcolem2  26586  plydivlem4  26610  leibpi  27263  chtublem  27531  sumdchr  27592  bposlem6  27609  lgsval  27621  dchrvmasumiflem2  27822  padicabvcxp  27952  mplasclco  34141  extvfv  34158  dfrdg3  36538  cbvsumdavw  37048  ftc1anclem2  38592  ftc1anclem5  38595  ftc1anclem7  38597  fsuppssindlem2  43600  fsuppssind  43601  mnringmulrvald  45210  hoidifhspval  47587  hoimbl  47610  veronesevald  50940