Theorem ifeq1d 4474

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

Syntax hints:   → wi 4   = wceq 1547  ifcif 4454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-un 3888  df-if 4455

This theorem is referenced by:  ifeq12d  4476  ifbieq1d  4479  ifeq1da  4486  rabsnif  4655  fsuppmptif  9302  cantnflem1  9601  sumeq2w  15645  cbvsum  15648  cbvsumv  15649  sumeq2sdv  15656  isumless  15801  prodeq2sdv  15879  prodss  15903  subgmulg  19107  evlslem2  22055  selvval  22096  dmatcrng  22485  scmatscmiddistr  22491  scmatcrng  22504  marrepfval  22543  mdetr0  22588  mdetunilem8  22602  madufval  22620  madugsum  22626  minmar1fval  22629  decpmatid  22753  monmatcollpw  22762  pmatcollpwscmatlem1  22772  cnmpopc  24913  pcoval2  25001  pcopt  25007  itgz  25766  iblss2  25791  itgss  25797  itgcn  25830  plyeq0lem  26193  dgrcolem2  26257  plydivlem4  26280  leibpi  26924  chtublem  27192  sumdchr  27253  bposlem6  27270  lgsval  27282  dchrvmasumiflem2  27483  padicabvcxp  27613  mplasclco  33700  extvfv  33717  dfrdg3  36022  cbvsumdavw  36507  matunitlindflem1  37983  ftc1anclem2  38061  ftc1anclem5  38064  ftc1anclem7  38066  fsuppssindlem2  43042  fsuppssind  43043  mnringmulrvald  44671  hoidifhspval  47051  hoimbl  47074