Theorem ifeq1d 4498

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

Syntax hints:   → wi 4   = wceq 1540  ifcif 4478

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 3397  df-v 3440  df-un 3910  df-if 4479

This theorem is referenced by:  ifeq12d  4500  ifbieq1d  4503  ifeq1da  4510  rabsnif  4677  fsuppmptif  9308  cantnflem1  9604  sumeq2w  15617  cbvsum  15620  cbvsumv  15621  sumeq2sdv  15628  isumless  15770  prodeq2sdv  15848  prodss  15872  subgmulg  19037  evlslem2  22002  selvval  22038  dmatcrng  22405  scmatscmiddistr  22411  scmatcrng  22424  marrepfval  22463  mdetr0  22508  mdetunilem8  22522  madufval  22540  madugsum  22546  minmar1fval  22549  decpmatid  22673  monmatcollpw  22682  pmatcollpwscmatlem1  22692  cnmpopc  24838  pcoval2  24932  pcopt  24938  itgz  25698  iblss2  25723  itgss  25729  itgcn  25762  plyeq0lem  26131  dgrcolem2  26196  plydivlem4  26220  leibpi  26868  chtublem  27138  sumdchr  27199  bposlem6  27216  lgsval  27228  dchrvmasumiflem2  27429  padicabvcxp  27559  dfrdg3  35772  cbvsumdavw  36255  matunitlindflem1  37598  ftc1anclem2  37676  ftc1anclem5  37679  ftc1anclem7  37681  fsuppssindlem2  42568  fsuppssind  42569  mnringmulrvald  44203  hoidifhspval  46593  hoimbl  46616