Theorem ifeq1d 4475

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

Syntax hints:   → wi 4   = wceq 1539  ifcif 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-un 3888  df-if 4457

This theorem is referenced by:  ifeq12d  4477  ifbieq1d  4480  ifeq1da  4487  rabsnif  4656  fsuppmptif  9088  cantnflem1  9377  sumeq2w  15332  cbvsum  15335  isumless  15485  prodss  15585  subgmulg  18684  evlslem2  21199  selvval  21238  dmatcrng  21559  scmatscmiddistr  21565  scmatcrng  21578  marrepfval  21617  mdetr0  21662  mdetunilem8  21676  madufval  21694  madugsum  21700  minmar1fval  21703  decpmatid  21827  monmatcollpw  21836  pmatcollpwscmatlem1  21846  cnmpopc  23997  pcoval2  24085  pcopt  24091  itgz  24850  iblss2  24875  itgss  24881  itgcn  24914  plyeq0lem  25276  dgrcolem2  25340  plydivlem4  25361  leibpi  25997  chtublem  26264  sumdchr  26325  bposlem6  26342  lgsval  26354  dchrvmasumiflem2  26555  padicabvcxp  26685  dfrdg3  33678  matunitlindflem1  35700  ftc1anclem2  35778  ftc1anclem5  35781  ftc1anclem7  35783  fsuppssindlem2  40204  fsuppssind  40205  mnringmulrvald  41734  hoidifhspval  44036  hoimbl  44059