Theorem ifeq12d 4500

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

Syntax hints:   → wi 4   = wceq 1540  ifcif 4478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-un 3910  df-if 4479

This theorem is referenced by:  ifbieq12d  4507  csbif  4536  oev  8439  dfac12r  10060  xaddpnf1  13146  swrdccat3blem  14663  relexpsucnnr  14950  ruclem1  16158  eucalgval  16511  gsumpropd  18570  gsumpropd2lem  18571  gsumress  18574  mulgfval  18966  mulgfvalALT  18967  mulgpropd  19013  frgpup3lem  19674  isobs  21645  uvcfval  21709  psrascl  21904  subrgmvr  21956  psdmvr  22072  rhmmpl  22286  rhmply1vr1  22290  matsc  22353  scmatscmide  22410  marrepval0  22464  marepvval0  22469  mulmarep1el  22475  madufval  22540  madugsum  22546  minmar1fval  22549  pmat1opsc  22602  pmat1ovscd  22603  mat2pmat1  22635  decpmatid  22673  idpm2idmp  22704  pcoval  24927  pcorevlem  24942  itg2const  25657  ditgeq3  25767  efrlim  26895  efrlimOLD  26896  lgsval  27228  rpvmasum2  27439  expsval  28335  fzto1st  33058  psgnfzto1st  33060  xrhval  33987  cbvditgdavw  36258  itg2addnclem  37653  ftc1anclem5  37679  hdmap1fval  41778  sticksstones12a  42133  sticksstones12  42134  rhmpsr  42528  selvvvval  42561  fsuppind  42566  dgrsub2  43111  reabssgn  43612  dirkerval  46076  fourierdlem111  46202  fourierdlem112  46203  fourierdlem113  46204  hsphoif  46561  hsphoival  46564  hoidmvlelem5  46584  hoidifhspval2  46600  hspmbllem2  46612  itcoval  48650