Theorem ifeq1d 4501

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

Syntax hints:   → wi 4   = wceq 1542  ifcif 4481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-un 3908  df-if 4482

This theorem is referenced by:  ifeq12d  4503  ifbieq1d  4506  ifeq1da  4513  rabsnif  4682  fsuppmptif  9314  cantnflem1  9610  sumeq2w  15627  cbvsum  15630  cbvsumv  15631  sumeq2sdv  15638  isumless  15780  prodeq2sdv  15858  prodss  15882  subgmulg  19082  evlslem2  22046  selvval  22090  dmatcrng  22458  scmatscmiddistr  22464  scmatcrng  22477  marrepfval  22516  mdetr0  22561  mdetunilem8  22575  madufval  22593  madugsum  22599  minmar1fval  22602  decpmatid  22726  monmatcollpw  22735  pmatcollpwscmatlem1  22745  cnmpopc  24890  pcoval2  24984  pcopt  24990  itgz  25750  iblss2  25775  itgss  25781  itgcn  25814  plyeq0lem  26183  dgrcolem2  26248  plydivlem4  26272  leibpi  26920  chtublem  27190  sumdchr  27251  bposlem6  27268  lgsval  27280  dchrvmasumiflem2  27481  padicabvcxp  27611  extvfv  33709  dfrdg3  36007  cbvsumdavw  36492  matunitlindflem1  37864  ftc1anclem2  37942  ftc1anclem5  37945  ftc1anclem7  37947  fsuppssindlem2  42947  fsuppssind  42948  mnringmulrvald  44580  hoidifhspval  46963  hoimbl  46986