Theorem ifeq1d 4504

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

Syntax hints:   → wi 4   = wceq 1540  ifcif 4484

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-un 3916  df-if 4485

This theorem is referenced by:  ifeq12d  4506  ifbieq1d  4509  ifeq1da  4516  rabsnif  4683  fsuppmptif  9326  cantnflem1  9618  sumeq2w  15634  cbvsum  15637  cbvsumv  15638  sumeq2sdv  15645  isumless  15787  prodeq2sdv  15865  prodss  15889  subgmulg  19048  evlslem2  21962  selvval  21998  dmatcrng  22365  scmatscmiddistr  22371  scmatcrng  22384  marrepfval  22423  mdetr0  22468  mdetunilem8  22482  madufval  22500  madugsum  22506  minmar1fval  22509  decpmatid  22633  monmatcollpw  22642  pmatcollpwscmatlem1  22652  cnmpopc  24798  pcoval2  24892  pcopt  24898  itgz  25658  iblss2  25683  itgss  25689  itgcn  25722  plyeq0lem  26091  dgrcolem2  26156  plydivlem4  26180  leibpi  26828  chtublem  27098  sumdchr  27159  bposlem6  27176  lgsval  27188  dchrvmasumiflem2  27389  padicabvcxp  27519  dfrdg3  35757  cbvsumdavw  36240  matunitlindflem1  37583  ftc1anclem2  37661  ftc1anclem5  37664  ftc1anclem7  37666  fsuppssindlem2  42553  fsuppssind  42554  mnringmulrvald  44189  hoidifhspval  46579  hoimbl  46602