Theorem ifeq12d 4507

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 4505	. 2 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐶))
3		ifeq12d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
4	3	ifeq2d 4506	. 2 ⊢ (𝜑 → if(𝜓, 𝐵, 𝐶) = if(𝜓, 𝐵, 𝐷))
5	2, 4	eqtrd 2797	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐷))

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ifcif 4485

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-un 3907  df-if 4486

This theorem is used by:  ifbieq12d  4514  csbif  4543  oev  8505  dfac12r  10153  xaddpnf1  13282  swrdccat3blem  14812  relexpsucnnr  15102  ruclem1  16325  eucalgval  16678  gsumpropd  18786  gsumpropd2lem  18787  gsumress  18790  mulgfval  19198  mulgfvalALT  19199  mulgpropd  19245  frgpup3lem  19910  isobs  21939  uvcfval  22003  psrascl  22199  subrgmvr  22255  selvvvval  22364  psdmvr  22403  rhmmpl  22611  rhmply1vr1  22615  matsc  22678  scmatscmide  22735  marrepval0  22789  marepvval0  22794  mulmarep1el  22800  madufval  22865  madugsum  22871  minmar1fval  22874  pmat1opsc  22930  pmat1ovscd  22931  mat2pmat1  22963  decpmatid  23001  idpm2idmp  23032  pcoval  25245  pcorevlem  25260  itg2const  25974  ditgeq3  26084  efrlim  27214  lgsval  27545  rpvmasum2  27756  expsval  28698  fzto1st  33551  psgnfzto1st  33553  mplasclco  34034  extvval  34049  esplyfval0  34082  xrhval  34536  cbvditgdavw  36910  itg2addnclem  38428  ftc1anclem5  38454  hdmap1fval  42677  sticksstones12a  43031  sticksstones12  43032  rhmpsr  43437  fsuppind  43444  dgrsub2  43984  reabssgn  44484  dirkerval  46927  fourierdlem111  47053  fourierdlem112  47054  fourierdlem113  47055  hsphoif  47412  hsphoival  47415  hoidmvlelem5  47435  hoidifhspval2  47451  hspmbllem2  47463  itcoval  49599  crosspval  50795  veronesematrowexpd  50823