Theorem ifeq12d 4514

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

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

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-un 3913  df-if 4493

This theorem is used by:  ifbieq12d  4521  csbif  4550  oev  8508  dfac12r  10149  xaddpnf1  13270  swrdccat3blem  14800  relexpsucnnr  15088  ruclem1  16312  eucalgval  16665  gsumpropd  18765  gsumpropd2lem  18766  gsumress  18769  mulgfval  19166  mulgfvalALT  19167  mulgpropd  19213  frgpup3lem  19878  isobs  21907  uvcfval  21971  psrascl  22165  subrgmvr  22221  selvvvval  22330  psdmvr  22369  rhmmpl  22577  rhmply1vr1  22581  matsc  22644  scmatscmide  22701  marrepval0  22755  marepvval0  22760  mulmarep1el  22766  madufval  22831  madugsum  22837  minmar1fval  22840  pmat1opsc  22893  pmat1ovscd  22894  mat2pmat1  22926  decpmatid  22964  idpm2idmp  22995  pcoval  25207  pcorevlem  25222  itg2const  25936  ditgeq3  26046  efrlim  27171  lgsval  27502  rpvmasum2  27713  expsval  28655  fzto1st  33454  psgnfzto1st  33456  mplasclco  33937  extvval  33952  esplyfval0  33985  xrhval  34439  cbvditgdavw  36835  itg2addnclem  38363  ftc1anclem5  38389  hdmap1fval  42611  sticksstones12a  42965  sticksstones12  42966  rhmpsr  43356  fsuppind  43363  dgrsub2  43903  reabssgn  44403  dirkerval  46846  fourierdlem111  46972  fourierdlem112  46973  fourierdlem113  46974  hsphoif  47331  hsphoival  47334  hoidmvlelem5  47354  hoidifhspval2  47370  hspmbllem2  47382  itcoval  49482  crosspval  50677