Theorem ifeq1d 4496

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

Syntax hints:   → wi 4   = wceq 1541  ifcif 4476

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 2115  ax-9 2123  ax-ext 2705

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 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-un 3903  df-if 4477

This theorem is referenced by:  ifeq12d  4498  ifbieq1d  4501  ifeq1da  4508  rabsnif  4677  fsuppmptif  9294  cantnflem1  9590  sumeq2w  15606  cbvsum  15609  cbvsumv  15610  sumeq2sdv  15617  isumless  15759  prodeq2sdv  15837  prodss  15861  subgmulg  19061  evlslem2  22025  selvval  22069  dmatcrng  22437  scmatscmiddistr  22443  scmatcrng  22456  marrepfval  22495  mdetr0  22540  mdetunilem8  22554  madufval  22572  madugsum  22578  minmar1fval  22581  decpmatid  22705  monmatcollpw  22714  pmatcollpwscmatlem1  22724  cnmpopc  24869  pcoval2  24963  pcopt  24969  itgz  25729  iblss2  25754  itgss  25760  itgcn  25793  plyeq0lem  26162  dgrcolem2  26227  plydivlem4  26251  leibpi  26899  chtublem  27169  sumdchr  27230  bposlem6  27247  lgsval  27259  dchrvmasumiflem2  27460  padicabvcxp  27590  extvfv  33626  dfrdg3  35910  cbvsumdavw  36395  matunitlindflem1  37729  ftc1anclem2  37807  ftc1anclem5  37810  ftc1anclem7  37812  fsuppssindlem2  42750  fsuppssind  42751  mnringmulrvald  44384  hoidifhspval  46768  hoimbl  46791