Theorem ifeq1d 4545

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

Syntax hints:   → wi 4   = wceq 1540  ifcif 4525

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-un 3956  df-if 4526

This theorem is referenced by:  ifeq12d  4547  ifbieq1d  4550  ifeq1da  4557  rabsnif  4723  fsuppmptif  9439  cantnflem1  9729  sumeq2w  15728  cbvsum  15731  cbvsumv  15732  sumeq2sdv  15739  isumless  15881  prodeq2sdv  15959  prodss  15983  subgmulg  19158  evlslem2  22103  selvval  22139  dmatcrng  22508  scmatscmiddistr  22514  scmatcrng  22527  marrepfval  22566  mdetr0  22611  mdetunilem8  22625  madufval  22643  madugsum  22649  minmar1fval  22652  decpmatid  22776  monmatcollpw  22785  pmatcollpwscmatlem1  22795  cnmpopc  24955  pcoval2  25049  pcopt  25055  itgz  25816  iblss2  25841  itgss  25847  itgcn  25880  plyeq0lem  26249  dgrcolem2  26314  plydivlem4  26338  leibpi  26985  chtublem  27255  sumdchr  27316  bposlem6  27333  lgsval  27345  dchrvmasumiflem2  27546  padicabvcxp  27676  dfrdg3  35797  cbvsumdavw  36280  matunitlindflem1  37623  ftc1anclem2  37701  ftc1anclem5  37704  ftc1anclem7  37706  fsuppssindlem2  42602  fsuppssind  42603  mnringmulrvald  44246  hoidifhspval  46623  hoimbl  46646