Theorem ifeq1d 4493

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

Syntax hints:   → wi 4   = wceq 1541  ifcif 4473

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 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3394  df-v 3436  df-un 3905  df-if 4474

This theorem is referenced by:  ifeq12d  4495  ifbieq1d  4498  ifeq1da  4505  rabsnif  4674  fsuppmptif  9278  cantnflem1  9574  sumeq2w  15591  cbvsum  15594  cbvsumv  15595  sumeq2sdv  15602  isumless  15744  prodeq2sdv  15822  prodss  15846  subgmulg  19045  evlslem2  22007  selvval  22043  dmatcrng  22410  scmatscmiddistr  22416  scmatcrng  22429  marrepfval  22468  mdetr0  22513  mdetunilem8  22527  madufval  22545  madugsum  22551  minmar1fval  22554  decpmatid  22678  monmatcollpw  22687  pmatcollpwscmatlem1  22697  cnmpopc  24842  pcoval2  24936  pcopt  24942  itgz  25702  iblss2  25727  itgss  25733  itgcn  25766  plyeq0lem  26135  dgrcolem2  26200  plydivlem4  26224  leibpi  26872  chtublem  27142  sumdchr  27203  bposlem6  27220  lgsval  27232  dchrvmasumiflem2  27433  padicabvcxp  27563  dfrdg3  35809  cbvsumdavw  36292  matunitlindflem1  37635  ftc1anclem2  37713  ftc1anclem5  37716  ftc1anclem7  37718  fsuppssindlem2  42604  fsuppssind  42605  mnringmulrvald  44239  hoidifhspval  46625  hoimbl  46648