Theorem ifeq1d 4442

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

Syntax hints:   → wi 4   = wceq 1538  ifcif 4423

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-rab 3079  df-v 3411  df-un 3865  df-if 4424

This theorem is referenced by:  ifeq12d  4444  ifbieq1d  4447  ifeq1da  4454  rabsnif  4619  fsuppmptif  8909  cantnflem1  9198  sumeq2w  15110  cbvsum  15113  isumless  15261  prodss  15362  subgmulg  18374  evlslem2  20856  selvval  20895  dmatcrng  21216  scmatscmiddistr  21222  scmatcrng  21235  marrepfval  21274  mdetr0  21319  mdetunilem8  21333  madufval  21351  madugsum  21357  minmar1fval  21360  decpmatid  21484  monmatcollpw  21493  pmatcollpwscmatlem1  21503  cnmpopc  23643  pcoval2  23731  pcopt  23737  itgz  24494  iblss2  24519  itgss  24525  itgcn  24558  plyeq0lem  24920  dgrcolem2  24984  plydivlem4  25005  leibpi  25641  chtublem  25908  sumdchr  25969  bposlem6  25986  lgsval  25998  dchrvmasumiflem2  26199  padicabvcxp  26329  dfrdg3  33301  matunitlindflem1  35368  ftc1anclem2  35446  ftc1anclem5  35449  ftc1anclem7  35451  fsuppssindlem2  39825  fsuppssind  39826  mnringmulrvald  41353  hoidifhspval  43658  hoimbl  43681