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 2795	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐷))

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ifcif 4481

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-un 4151  df-if 4482

This theorem is used by:  ifbieq12d  4510  csbif  4539  oev  8526  dfac12r  10229  xaddpnf1  13360  swrdccat3blem  14893  relexpsucnnr  15184  ruclem1  16405  eucalgval  16763  gsumpropd  18873  gsumpropd2lem  18874  gsumress  18877  mulgfval  19285  mulgfvalALT  19286  mulgpropd  19332  frgpup3lem  19997  isobs  22032  uvcfval  22096  psrascl  22292  subrgmvr  22348  selvvvval  22457  psdmvr  22496  rhmmpl  22704  rhmply1vr1  22708  matsc  22771  scmatscmide  22828  marrepval0  22882  marepvval0  22887  mulmarep1el  22893  madufval  22958  madugsum  22964  minmar1fval  22967  pmat1opsc  23023  pmat1ovscd  23024  mat2pmat1  23056  decpmatid  23094  idpm2idmp  23125  pcoval  25338  pcorevlem  25353  itg2const  26067  ditgeq3  26176  efrlim  27303  lgsval  27634  rpvmasum2  27845  expsval  28817  fzto1st  33711  psgnfzto1st  33713  mplasclco  34195  extvval  34210  esplyfval0  34243  xrhval  34697  cbvditgdavw  37164  itg2addnclem  38683  ftc1anclem5  38709  hdmap1fval  42947  sticksstones12a  43301  sticksstones12  43302  rhmpsr  43705  fsuppind  43712  dgrsub2  44231  reabssgn  44730  dirkerval  47195  fourierdlem111  47321  fourierdlem112  47322  fourierdlem113  47323  hsphoif  47680  hsphoival  47683  hoidmvlelem5  47703  hoidifhspval2  47719  hspmbllem2  47731  itcoval  49867  crosspval  51123  veronesematrowexpd  51151