Theorem ifeq1d 4548

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

Syntax hints:   → wi 4   = wceq 1542  ifcif 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-un 3954  df-if 4530

This theorem is referenced by:  ifeq12d  4550  ifbieq1d  4553  ifeq1da  4560  rabsnif  4728  fsuppmptif  9394  cantnflem1  9684  sumeq2w  15638  cbvsum  15641  isumless  15791  prodss  15891  subgmulg  19020  evlslem2  21642  selvval  21681  dmatcrng  22004  scmatscmiddistr  22010  scmatcrng  22023  marrepfval  22062  mdetr0  22107  mdetunilem8  22121  madufval  22139  madugsum  22145  minmar1fval  22148  decpmatid  22272  monmatcollpw  22281  pmatcollpwscmatlem1  22291  cnmpopc  24444  pcoval2  24532  pcopt  24538  itgz  25298  iblss2  25323  itgss  25329  itgcn  25362  plyeq0lem  25724  dgrcolem2  25788  plydivlem4  25809  leibpi  26447  chtublem  26714  sumdchr  26775  bposlem6  26792  lgsval  26804  dchrvmasumiflem2  27005  padicabvcxp  27135  dfrdg3  34768  matunitlindflem1  36484  ftc1anclem2  36562  ftc1anclem5  36565  ftc1anclem7  36567  fsuppssindlem2  41164  fsuppssind  41165  mnringmulrvald  42986  hoidifhspval  45324  hoimbl  45347