Theorem ifeq1d 4520

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

Syntax hints:   → wi 4   = wceq 1540  ifcif 4500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-un 3931  df-if 4501

This theorem is referenced by:  ifeq12d  4522  ifbieq1d  4525  ifeq1da  4532  rabsnif  4699  fsuppmptif  9411  cantnflem1  9703  sumeq2w  15708  cbvsum  15711  cbvsumv  15712  sumeq2sdv  15719  isumless  15861  prodeq2sdv  15939  prodss  15963  subgmulg  19123  evlslem2  22037  selvval  22073  dmatcrng  22440  scmatscmiddistr  22446  scmatcrng  22459  marrepfval  22498  mdetr0  22543  mdetunilem8  22557  madufval  22575  madugsum  22581  minmar1fval  22584  decpmatid  22708  monmatcollpw  22717  pmatcollpwscmatlem1  22727  cnmpopc  24873  pcoval2  24967  pcopt  24973  itgz  25734  iblss2  25759  itgss  25765  itgcn  25798  plyeq0lem  26167  dgrcolem2  26232  plydivlem4  26256  leibpi  26904  chtublem  27174  sumdchr  27235  bposlem6  27252  lgsval  27264  dchrvmasumiflem2  27465  padicabvcxp  27595  dfrdg3  35814  cbvsumdavw  36297  matunitlindflem1  37640  ftc1anclem2  37718  ftc1anclem5  37721  ftc1anclem7  37723  fsuppssindlem2  42615  fsuppssind  42616  mnringmulrvald  44251  hoidifhspval  46637  hoimbl  46660