Theorem ifeq1d 4490

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

Syntax hints:   → wi 4   = wceq 1541  ifcif 4470

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-un 3902  df-if 4471

This theorem is referenced by:  ifeq12d  4492  ifbieq1d  4495  ifeq1da  4502  rabsnif  4671  fsuppmptif  9278  cantnflem1  9574  sumeq2w  15594  cbvsum  15597  cbvsumv  15598  sumeq2sdv  15605  isumless  15747  prodeq2sdv  15825  prodss  15849  subgmulg  19048  evlslem2  22009  selvval  22045  dmatcrng  22412  scmatscmiddistr  22418  scmatcrng  22431  marrepfval  22470  mdetr0  22515  mdetunilem8  22529  madufval  22547  madugsum  22553  minmar1fval  22556  decpmatid  22680  monmatcollpw  22689  pmatcollpwscmatlem1  22699  cnmpopc  24844  pcoval2  24938  pcopt  24944  itgz  25704  iblss2  25729  itgss  25735  itgcn  25768  plyeq0lem  26137  dgrcolem2  26202  plydivlem4  26226  leibpi  26874  chtublem  27144  sumdchr  27205  bposlem6  27222  lgsval  27234  dchrvmasumiflem2  27435  padicabvcxp  27565  dfrdg3  35830  cbvsumdavw  36313  matunitlindflem1  37656  ftc1anclem2  37734  ftc1anclem5  37737  ftc1anclem7  37739  fsuppssindlem2  42625  fsuppssind  42626  mnringmulrvald  44260  hoidifhspval  46646  hoimbl  46669