Theorem ifeq1d 4508

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

Syntax hints:   → wi 4   = wceq 1570  ifcif 4488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-un 3911  df-if 4489

This theorem is referenced by:  ifeq12d  4510  ifbieq1d  4513  ifeq1da  4520  rabsnif  4690  fsuppmptif  9360  cantnflem1  9659  sumeq2w  15745  cbvsum  15748  cbvsumv  15749  sumeq2sdv  15756  isumless  15901  prodeq2sdv  15979  prodss  16003  subgmulg  19208  evlslem2  22211  selvval  22252  dmatcrng  22640  scmatscmiddistr  22646  scmatcrng  22659  marrepfval  22698  mdetr0  22743  mdetunilem8  22757  madufval  22775  madugsum  22781  minmar1fval  22784  decpmatid  22908  monmatcollpw  22917  pmatcollpwscmatlem1  22927  cnmpopc  25068  pcoval2  25156  pcopt  25162  itgz  25921  iblss2  25946  itgss  25952  itgcn  25985  plyeq0lem  26348  dgrcolem2  26412  plydivlem4  26438  leibpi  27088  chtublem  27356  sumdchr  27417  bposlem6  27434  lgsval  27446  dchrvmasumiflem2  27647  padicabvcxp  27777  mplasclco  33887  extvfv  33904  dfrdg3  36267  cbvsumdavw  36772  matunitlindflem1  38248  ftc1anclem2  38326  ftc1anclem5  38329  ftc1anclem7  38331  fsuppssindlem2  43307  fsuppssind  43308  mnringmulrvald  44934  hoidifhspval  47305  hoimbl  47328