Theorem ifeq12d 4503

Description: Equality deduction for conditional operator. (Contributed by NM, 24-Mar-2015.)

Hypotheses

Ref	Expression
ifeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
ifeq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
ifeq12d	⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐷))

Proof of Theorem ifeq12d

Step	Hyp	Ref	Expression
1		ifeq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	ifeq1d 4501	. 2 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3		ifeq12d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	3	ifeq2d 4502	. 2 ⊢ (𝜑 → if(𝜓, 𝐵, 𝐶) = if(𝜓, 𝐵, 𝐷))
5	2, 4	eqtrd 2772	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐷))

Syntax hints:   → wi 4   = wceq 1542  ifcif 4481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-un 3908  df-if 4482

This theorem is referenced by:  ifbieq12d  4510  csbif  4539  oev  8451  dfac12r  10069  xaddpnf1  13153  swrdccat3blem  14674  relexpsucnnr  14960  ruclem1  16168  eucalgval  16521  gsumpropd  18615  gsumpropd2lem  18616  gsumress  18619  mulgfval  19011  mulgfvalALT  19012  mulgpropd  19058  frgpup3lem  19718  isobs  21687  uvcfval  21751  psrascl  21946  subrgmvr  22000  psdmvr  22124  rhmmpl  22339  rhmply1vr1  22343  matsc  22406  scmatscmide  22463  marrepval0  22517  marepvval0  22522  mulmarep1el  22528  madufval  22593  madugsum  22599  minmar1fval  22602  pmat1opsc  22655  pmat1ovscd  22656  mat2pmat1  22688  decpmatid  22726  idpm2idmp  22757  pcoval  24979  pcorevlem  24994  itg2const  25709  ditgeq3  25819  efrlim  26947  efrlimOLD  26948  lgsval  27280  rpvmasum2  27491  expsval  28433  fzto1st  33196  psgnfzto1st  33198  extvval  33707  esplyfval0  33740  xrhval  34195  cbvditgdavw  36495  itg2addnclem  37919  ftc1anclem5  37945  hdmap1fval  42169  sticksstones12a  42524  sticksstones12  42525  rhmpsr  42917  selvvvval  42940  fsuppind  42945  dgrsub2  43489  reabssgn  43989  dirkerval  46446  fourierdlem111  46572  fourierdlem112  46573  fourierdlem113  46574  hsphoif  46931  hsphoival  46934  hoidmvlelem5  46954  hoidifhspval2  46970  hspmbllem2  46982  itcoval  49018