Theorem ifeq1d 4510

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

Syntax hints:   → wi 4   = wceq 1541  ifcif 4491

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-un 3918  df-if 4492

This theorem is referenced by:  ifeq12d  4512  ifbieq1d  4515  ifeq1da  4522  rabsnif  4689  fsuppmptif  9344  cantnflem1  9634  sumeq2w  15588  cbvsum  15591  isumless  15741  prodss  15841  subgmulg  18956  evlslem2  21526  selvval  21565  dmatcrng  21888  scmatscmiddistr  21894  scmatcrng  21907  marrepfval  21946  mdetr0  21991  mdetunilem8  22005  madufval  22023  madugsum  22029  minmar1fval  22032  decpmatid  22156  monmatcollpw  22165  pmatcollpwscmatlem1  22175  cnmpopc  24328  pcoval2  24416  pcopt  24422  itgz  25182  iblss2  25207  itgss  25213  itgcn  25246  plyeq0lem  25608  dgrcolem2  25672  plydivlem4  25693  leibpi  26329  chtublem  26596  sumdchr  26657  bposlem6  26674  lgsval  26686  dchrvmasumiflem2  26887  padicabvcxp  27017  dfrdg3  34457  matunitlindflem1  36147  ftc1anclem2  36225  ftc1anclem5  36228  ftc1anclem7  36230  fsuppssindlem2  40825  fsuppssind  40826  mnringmulrvald  42629  hoidifhspval  44969  hoimbl  44992