Theorem ifeq1d 4505

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-un 4154  df-if 4486

This theorem is used by:  ifeq12d  4507  ifbieq1d  4510  ifeq1da  4517  rabsnif  4686  fsuppmptif  9428  cantnflem1  9727  sumeq2w  15903  cbvsum  15906  cbvsumv  15907  sumeq2sdv  15914  isumless  16058  prodeq2sdv  16135  prodss  16158  subgmulg  19401  evlslem2  22443  selvval  22484  dmatcrng  22872  scmatscmiddistr  22878  scmatcrng  22891  marrepfval  22930  mdetr0  22975  mdetunilem8  22989  madufval  23007  madugsum  23013  minmar1fval  23016  matunitlindflem1  23049  decpmatid  23143  monmatcollpw  23152  pmatcollpwscmatlem1  23162  cnmpopc  25304  pcoval2  25392  pcopt  25398  itgz  26156  iblss2  26181  itgss  26187  itgcn  26220  plyeq0lem  26584  dgrcolem2  26648  plydivlem4  26672  leibpi  27327  chtublem  27595  sumdchr  27656  bposlem6  27673  lgsval  27685  dchrvmasumiflem2  27886  padicabvcxp  28016  mplasclco  34259  extvfv  34276  dfrdg3  36773  cbvsumdavw  37283  ftc1anclem2  38880  ftc1anclem5  38883  ftc1anclem7  38885  fsuppssindlem2  43886  fsuppssind  43887  mnringmulrvald  45486  hoidifhspval  47891  hoimbl  47914  veronesevald  51399