Theorem ifeq1d 4443

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

Syntax hints:   → wi 4   = wceq 1538  ifcif 4425

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-un 3886  df-if 4426

This theorem is referenced by:  ifeq12d  4445  ifbieq1d  4448  ifeq1da  4455  rabsnif  4619  fsuppmptif  8847  cantnflem1  9136  sumeq2w  15041  cbvsum  15044  isumless  15192  prodss  15293  subgmulg  18285  evlslem2  20751  selvval  20790  dmatcrng  21107  scmatscmiddistr  21113  scmatcrng  21126  marrepfval  21165  mdetr0  21210  mdetunilem8  21224  madufval  21242  madugsum  21248  minmar1fval  21251  decpmatid  21375  monmatcollpw  21384  pmatcollpwscmatlem1  21394  cnmpopc  23533  pcoval2  23621  pcopt  23627  itgz  24384  iblss2  24409  itgss  24415  itgcn  24448  plyeq0lem  24807  dgrcolem2  24871  plydivlem4  24892  leibpi  25528  chtublem  25795  sumdchr  25856  bposlem6  25873  lgsval  25885  dchrvmasumiflem2  26086  padicabvcxp  26216  dfrdg3  33154  matunitlindflem1  35053  ftc1anclem2  35131  ftc1anclem5  35134  ftc1anclem7  35136  fsuppssindlem2  39458  fsuppssind  39459  mnringmulrvald  40935  hoidifhspval  43247  hoimbl  43270