Theorem ifeq1d 4497

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

Syntax hints:   → wi 4   = wceq 1559  ifcif 4477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-un 3907  df-if 4478

This theorem is referenced by:  ifeq12d  4499  ifbieq1d  4502  ifeq1da  4509  rabsnif  4679  fsuppmptif  9339  cantnflem1  9638  sumeq2w  15710  cbvsum  15713  cbvsumv  15714  sumeq2sdv  15721  isumless  15866  prodeq2sdv  15944  prodss  15968  subgmulg  19173  evlslem2  22120  selvval  22161  dmatcrng  22550  scmatscmiddistr  22556  scmatcrng  22569  marrepfval  22608  mdetr0  22653  mdetunilem8  22667  madufval  22685  madugsum  22691  minmar1fval  22694  decpmatid  22818  monmatcollpw  22827  pmatcollpwscmatlem1  22837  cnmpopc  24978  pcoval2  25066  pcopt  25072  itgz  25831  iblss2  25856  itgss  25862  itgcn  25895  plyeq0lem  26258  dgrcolem2  26322  plydivlem4  26348  leibpi  26995  chtublem  27263  sumdchr  27324  bposlem6  27341  lgsval  27353  dchrvmasumiflem2  27554  padicabvcxp  27684  mplasclco  33774  extvfv  33791  dfrdg3  36105  cbvsumdavw  36600  matunitlindflem1  38076  ftc1anclem2  38154  ftc1anclem5  38157  ftc1anclem7  38159  fsuppssindlem2  43135  fsuppssind  43136  mnringmulrvald  44764  hoidifhspval  47143  hoimbl  47166