Theorem ifeq12d 4499

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

Syntax hints:   → wi 4   = wceq 1559  ifcif 4477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-un 3907  df-if 4478

This theorem is referenced by:  ifbieq12d  4506  csbif  4535  oev  8476  dfac12r  10096  xaddpnf1  13222  swrdccat3blem  14745  relexpsucnnr  15031  ruclem1  16253  eucalgval  16606  gsumpropd  18702  gsumpropd2lem  18703  gsumress  18706  mulgfval  19101  mulgfvalALT  19102  mulgpropd  19148  frgpup3lem  19807  isobs  21759  uvcfval  21823  psrascl  22017  subrgmvr  22073  selvvvval  22182  psdmvr  22221  rhmmpl  22430  rhmply1vr1  22434  matsc  22497  scmatscmide  22554  marrepval0  22608  marepvval0  22613  mulmarep1el  22619  madufval  22684  madugsum  22690  minmar1fval  22693  pmat1opsc  22746  pmat1ovscd  22747  mat2pmat1  22779  decpmatid  22817  idpm2idmp  22848  pcoval  25060  pcorevlem  25075  itg2const  25789  ditgeq3  25899  efrlim  27021  lgsval  27352  rpvmasum2  27563  expsval  28505  fzto1st  33243  psgnfzto1st  33245  mplasclco  33773  extvval  33788  esplyfval0  33821  xrhval  34275  cbvditgdavw  36602  itg2addnclem  38130  ftc1anclem5  38156  hdmap1fval  42380  sticksstones12a  42734  sticksstones12  42735  rhmpsr  43125  fsuppind  43132  dgrsub2  43672  reabssgn  44172  dirkerval  46625  fourierdlem111  46751  fourierdlem112  46752  fourierdlem113  46753  hsphoif  47110  hsphoival  47113  hoidmvlelem5  47133  hoidifhspval2  47149  hspmbllem2  47161  itcoval  49243