Theorem ifeq1d 4511

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

Syntax hints:   → wi 4   = wceq 1540  ifcif 4491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-un 3922  df-if 4492

This theorem is referenced by:  ifeq12d  4513  ifbieq1d  4516  ifeq1da  4523  rabsnif  4690  fsuppmptif  9357  cantnflem1  9649  sumeq2w  15665  cbvsum  15668  cbvsumv  15669  sumeq2sdv  15676  isumless  15818  prodeq2sdv  15896  prodss  15920  subgmulg  19079  evlslem2  21993  selvval  22029  dmatcrng  22396  scmatscmiddistr  22402  scmatcrng  22415  marrepfval  22454  mdetr0  22499  mdetunilem8  22513  madufval  22531  madugsum  22537  minmar1fval  22540  decpmatid  22664  monmatcollpw  22673  pmatcollpwscmatlem1  22683  cnmpopc  24829  pcoval2  24923  pcopt  24929  itgz  25689  iblss2  25714  itgss  25720  itgcn  25753  plyeq0lem  26122  dgrcolem2  26187  plydivlem4  26211  leibpi  26859  chtublem  27129  sumdchr  27190  bposlem6  27207  lgsval  27219  dchrvmasumiflem2  27420  padicabvcxp  27550  dfrdg3  35791  cbvsumdavw  36274  matunitlindflem1  37617  ftc1anclem2  37695  ftc1anclem5  37698  ftc1anclem7  37700  fsuppssindlem2  42587  fsuppssind  42588  mnringmulrvald  44223  hoidifhspval  46613  hoimbl  46636