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(𝜓, 𝐵, 𝐶))

Syntax hints:   → wi 4   = wceq 1567  ifcif 4489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-un 3918  df-if 4490

This theorem is referenced by:  ifeq12d  4511  ifbieq1d  4514  ifeq1da  4521  rabsnif  4691  fsuppmptif  9355  cantnflem1  9654  sumeq2w  15739  cbvsum  15742  cbvsumv  15743  sumeq2sdv  15750  isumless  15895  prodeq2sdv  15973  prodss  15997  subgmulg  19203  evlslem2  22195  selvval  22236  dmatcrng  22624  scmatscmiddistr  22630  scmatcrng  22643  marrepfval  22682  mdetr0  22727  mdetunilem8  22741  madufval  22759  madugsum  22765  minmar1fval  22768  decpmatid  22892  monmatcollpw  22901  pmatcollpwscmatlem1  22911  cnmpopc  25052  pcoval2  25140  pcopt  25146  itgz  25905  iblss2  25930  itgss  25936  itgcn  25969  plyeq0lem  26332  dgrcolem2  26396  plydivlem4  26422  leibpi  27069  chtublem  27337  sumdchr  27398  bposlem6  27415  lgsval  27427  dchrvmasumiflem2  27628  padicabvcxp  27758  mplasclco  33847  extvfv  33864  dfrdg3  36181  cbvsumdavw  36676  matunitlindflem1  38150  ftc1anclem2  38228  ftc1anclem5  38231  ftc1anclem7  38233  fsuppssindlem2  43209  fsuppssind  43210  mnringmulrvald  44836  hoidifhspval  47207  hoimbl  47230