Theorem ifeq1d 4548

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

Syntax hints:   → wi 4   = wceq 1539  ifcif 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-rab 3431  df-v 3474  df-un 3954  df-if 4530

This theorem is referenced by:  ifeq12d  4550  ifbieq1d  4553  ifeq1da  4560  rabsnif  4728  fsuppmptif  9398  cantnflem1  9688  sumeq2w  15644  cbvsum  15647  isumless  15797  prodss  15897  subgmulg  19058  evlslem2  21863  selvval  21902  dmatcrng  22226  scmatscmiddistr  22232  scmatcrng  22245  marrepfval  22284  mdetr0  22329  mdetunilem8  22343  madufval  22361  madugsum  22367  minmar1fval  22370  decpmatid  22494  monmatcollpw  22503  pmatcollpwscmatlem1  22513  cnmpopc  24671  pcoval2  24765  pcopt  24771  itgz  25532  iblss2  25557  itgss  25563  itgcn  25596  plyeq0lem  25958  dgrcolem2  26022  plydivlem4  26043  leibpi  26681  chtublem  26948  sumdchr  27009  bposlem6  27026  lgsval  27038  dchrvmasumiflem2  27239  padicabvcxp  27369  dfrdg3  35070  matunitlindflem1  36789  ftc1anclem2  36867  ftc1anclem5  36870  ftc1anclem7  36872  fsuppssindlem2  41468  fsuppssind  41469  mnringmulrvald  43290  hoidifhspval  45624  hoimbl  45647