Theorem ifeq1d 4486

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

Syntax hints:   → wi 4   = wceq 1542  ifcif 4466

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-un 3894  df-if 4467

This theorem is referenced by:  ifeq12d  4488  ifbieq1d  4491  ifeq1da  4498  rabsnif  4667  fsuppmptif  9312  cantnflem1  9610  sumeq2w  15654  cbvsum  15657  cbvsumv  15658  sumeq2sdv  15665  isumless  15810  prodeq2sdv  15888  prodss  15912  subgmulg  19116  evlslem2  22057  selvval  22101  dmatcrng  22467  scmatscmiddistr  22473  scmatcrng  22486  marrepfval  22525  mdetr0  22570  mdetunilem8  22584  madufval  22602  madugsum  22608  minmar1fval  22611  decpmatid  22735  monmatcollpw  22744  pmatcollpwscmatlem1  22754  cnmpopc  24895  pcoval2  24983  pcopt  24989  itgz  25748  iblss2  25773  itgss  25779  itgcn  25812  plyeq0lem  26175  dgrcolem2  26239  plydivlem4  26262  leibpi  26906  chtublem  27174  sumdchr  27235  bposlem6  27252  lgsval  27264  dchrvmasumiflem2  27465  padicabvcxp  27595  extvfv  33677  dfrdg3  35976  cbvsumdavw  36461  matunitlindflem1  37937  ftc1anclem2  38015  ftc1anclem5  38018  ftc1anclem7  38020  fsuppssindlem2  43025  fsuppssind  43026  mnringmulrvald  44654  hoidifhspval  47036  hoimbl  47059