Theorem ifeq1d 4478

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

Syntax hints:   → wi 4   = wceq 1539  ifcif 4459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-un 3892  df-if 4460

This theorem is referenced by:  ifeq12d  4480  ifbieq1d  4483  ifeq1da  4490  rabsnif  4659  fsuppmptif  9158  cantnflem1  9447  sumeq2w  15404  cbvsum  15407  isumless  15557  prodss  15657  subgmulg  18769  evlslem2  21289  selvval  21328  dmatcrng  21651  scmatscmiddistr  21657  scmatcrng  21670  marrepfval  21709  mdetr0  21754  mdetunilem8  21768  madufval  21786  madugsum  21792  minmar1fval  21795  decpmatid  21919  monmatcollpw  21928  pmatcollpwscmatlem1  21938  cnmpopc  24091  pcoval2  24179  pcopt  24185  itgz  24945  iblss2  24970  itgss  24976  itgcn  25009  plyeq0lem  25371  dgrcolem2  25435  plydivlem4  25456  leibpi  26092  chtublem  26359  sumdchr  26420  bposlem6  26437  lgsval  26449  dchrvmasumiflem2  26650  padicabvcxp  26780  dfrdg3  33772  matunitlindflem1  35773  ftc1anclem2  35851  ftc1anclem5  35854  ftc1anclem7  35856  fsuppssindlem2  40281  fsuppssind  40282  mnringmulrvald  41845  hoidifhspval  44146  hoimbl  44169