Theorem ifeq1d 4550

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

Syntax hints:   → wi 4   = wceq 1537  ifcif 4531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-un 3968  df-if 4532

This theorem is referenced by:  ifeq12d  4552  ifbieq1d  4555  ifeq1da  4562  rabsnif  4728  fsuppmptif  9437  cantnflem1  9727  sumeq2w  15725  cbvsum  15728  cbvsumv  15729  sumeq2sdv  15736  isumless  15878  prodeq2sdv  15956  prodss  15980  subgmulg  19171  evlslem2  22121  selvval  22157  dmatcrng  22524  scmatscmiddistr  22530  scmatcrng  22543  marrepfval  22582  mdetr0  22627  mdetunilem8  22641  madufval  22659  madugsum  22665  minmar1fval  22668  decpmatid  22792  monmatcollpw  22801  pmatcollpwscmatlem1  22811  cnmpopc  24969  pcoval2  25063  pcopt  25069  itgz  25831  iblss2  25856  itgss  25862  itgcn  25895  plyeq0lem  26264  dgrcolem2  26329  plydivlem4  26353  leibpi  27000  chtublem  27270  sumdchr  27331  bposlem6  27348  lgsval  27360  dchrvmasumiflem2  27561  padicabvcxp  27691  dfrdg3  35778  cbvsumdavw  36262  matunitlindflem1  37603  ftc1anclem2  37681  ftc1anclem5  37684  ftc1anclem7  37686  fsuppssindlem2  42579  fsuppssind  42580  mnringmulrvald  44223  hoidifhspval  46564  hoimbl  46587