Theorem ifeq12d 4527

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

Syntax hints:   → wi 4   = wceq 1540  ifcif 4505

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-un 3936  df-if 4506

This theorem is referenced by:  ifbieq12d  4534  csbif  4563  oev  8531  dfac12r  10166  xaddpnf1  13247  swrdccat3blem  14762  relexpsucnnr  15049  ruclem1  16254  eucalgval  16606  gsumpropd  18661  gsumpropd2lem  18662  gsumress  18665  mulgfval  19057  mulgfvalALT  19058  mulgpropd  19104  frgpup3lem  19763  isobs  21685  uvcfval  21749  psrascl  21944  subrgmvr  21996  psdmvr  22112  rhmmpl  22326  rhmply1vr1  22330  matsc  22393  scmatscmide  22450  marrepval0  22504  marepvval0  22509  mulmarep1el  22515  madufval  22580  madugsum  22586  minmar1fval  22589  pmat1opsc  22642  pmat1ovscd  22643  mat2pmat1  22675  decpmatid  22713  idpm2idmp  22744  pcoval  24967  pcorevlem  24982  itg2const  25698  ditgeq3  25808  efrlim  26936  efrlimOLD  26937  lgsval  27269  rpvmasum2  27480  expsval  28368  fzto1st  33119  psgnfzto1st  33121  xrhval  34054  cbvditgdavw  36305  itg2addnclem  37700  ftc1anclem5  37726  hdmap1fval  41820  sticksstones12a  42175  sticksstones12  42176  rhmpsr  42550  selvvvval  42583  fsuppind  42588  dgrsub2  43134  reabssgn  43635  dirkerval  46100  fourierdlem111  46226  fourierdlem112  46227  fourierdlem113  46228  hsphoif  46585  hsphoival  46588  hoidmvlelem5  46608  hoidifhspval2  46624  hspmbllem2  46636  itcoval  48621