Theorem ifeq1d 4509

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-un 3911  df-if 4490

This theorem is used by:  ifeq12d  4511  ifbieq1d  4514  ifeq1da  4521  rabsnif  4691  fsuppmptif  9362  cantnflem1  9661  sumeq2w  15763  cbvsum  15766  cbvsumv  15767  sumeq2sdv  15774  isumless  15918  prodeq2sdv  15996  prodss  16020  subgmulg  19231  evlslem2  22260  selvval  22301  dmatcrng  22689  scmatscmiddistr  22695  scmatcrng  22708  marrepfval  22747  mdetr0  22792  mdetunilem8  22806  madufval  22824  madugsum  22830  minmar1fval  22833  decpmatid  22957  monmatcollpw  22966  pmatcollpwscmatlem1  22976  cnmpopc  25118  pcoval2  25206  pcopt  25212  itgz  25971  iblss2  25996  itgss  26002  itgcn  26035  plyeq0lem  26398  dgrcolem2  26462  plydivlem4  26488  leibpi  27138  chtublem  27406  sumdchr  27467  bposlem6  27484  lgsval  27496  dchrvmasumiflem2  27697  padicabvcxp  27827  mplasclco  33946  extvfv  33963  dfrdg3  36299  cbvsumdavw  36824  matunitlindflem1  38300  ftc1anclem2  38378  ftc1anclem5  38381  ftc1anclem7  38383  fsuppssindlem2  43357  fsuppssind  43358  mnringmulrvald  44984  hoidifhspval  47355  hoimbl  47378