Theorem ifeq1d 4499

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

Syntax hints:   → wi 4   = wceq 1541  ifcif 4479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-un 3906  df-if 4480

This theorem is referenced by:  ifeq12d  4501  ifbieq1d  4504  ifeq1da  4511  rabsnif  4680  fsuppmptif  9302  cantnflem1  9598  sumeq2w  15615  cbvsum  15618  cbvsumv  15619  sumeq2sdv  15626  isumless  15768  prodeq2sdv  15846  prodss  15870  subgmulg  19070  evlslem2  22034  selvval  22078  dmatcrng  22446  scmatscmiddistr  22452  scmatcrng  22465  marrepfval  22504  mdetr0  22549  mdetunilem8  22563  madufval  22581  madugsum  22587  minmar1fval  22590  decpmatid  22714  monmatcollpw  22723  pmatcollpwscmatlem1  22733  cnmpopc  24878  pcoval2  24972  pcopt  24978  itgz  25738  iblss2  25763  itgss  25769  itgcn  25802  plyeq0lem  26171  dgrcolem2  26236  plydivlem4  26260  leibpi  26908  chtublem  27178  sumdchr  27239  bposlem6  27256  lgsval  27268  dchrvmasumiflem2  27469  padicabvcxp  27599  extvfv  33698  dfrdg3  35988  cbvsumdavw  36473  matunitlindflem1  37817  ftc1anclem2  37895  ftc1anclem5  37898  ftc1anclem7  37900  fsuppssindlem2  42835  fsuppssind  42836  mnringmulrvald  44468  hoidifhspval  46852  hoimbl  46875