Theorem ifeq1d 4552

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

Syntax hints:   → wi 4   = wceq 1534  ifcif 4533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420  df-v 3464  df-un 3952  df-if 4534

This theorem is referenced by:  ifeq12d  4554  ifbieq1d  4557  ifeq1da  4564  rabsnif  4732  fsuppmptif  9442  cantnflem1  9732  sumeq2w  15696  cbvsum  15699  isumless  15849  prodss  15949  subgmulg  19134  evlslem2  22094  selvval  22130  dmatcrng  22495  scmatscmiddistr  22501  scmatcrng  22514  marrepfval  22553  mdetr0  22598  mdetunilem8  22612  madufval  22630  madugsum  22636  minmar1fval  22639  decpmatid  22763  monmatcollpw  22772  pmatcollpwscmatlem1  22782  cnmpopc  24940  pcoval2  25034  pcopt  25040  itgz  25801  iblss2  25826  itgss  25832  itgcn  25865  plyeq0lem  26237  dgrcolem2  26302  plydivlem4  26324  leibpi  26970  chtublem  27240  sumdchr  27301  bposlem6  27318  lgsval  27330  dchrvmasumiflem2  27531  padicabvcxp  27661  dfrdg3  35620  matunitlindflem1  37317  ftc1anclem2  37395  ftc1anclem5  37398  ftc1anclem7  37400  fsuppssindlem2  42064  fsuppssind  42065  mnringmulrvald  43901  hoidifhspval  46229  hoimbl  46252