Theorem ifeq12d 4501

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

Syntax hints:   → wi 4   = wceq 1541  ifcif 4479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-un 3906  df-if 4480

This theorem is referenced by:  ifbieq12d  4508  csbif  4537  oev  8441  dfac12r  10057  xaddpnf1  13141  swrdccat3blem  14662  relexpsucnnr  14948  ruclem1  16156  eucalgval  16509  gsumpropd  18603  gsumpropd2lem  18604  gsumress  18607  mulgfval  18999  mulgfvalALT  19000  mulgpropd  19046  frgpup3lem  19706  isobs  21675  uvcfval  21739  psrascl  21934  subrgmvr  21988  psdmvr  22112  rhmmpl  22327  rhmply1vr1  22331  matsc  22394  scmatscmide  22451  marrepval0  22505  marepvval0  22510  mulmarep1el  22516  madufval  22581  madugsum  22587  minmar1fval  22590  pmat1opsc  22643  pmat1ovscd  22644  mat2pmat1  22676  decpmatid  22714  idpm2idmp  22745  pcoval  24967  pcorevlem  24982  itg2const  25697  ditgeq3  25807  efrlim  26935  efrlimOLD  26936  lgsval  27268  rpvmasum2  27479  expsval  28421  fzto1st  33185  psgnfzto1st  33187  extvval  33696  esplyfval0  33722  xrhval  34175  cbvditgdavw  36476  itg2addnclem  37872  ftc1anclem5  37898  hdmap1fval  42056  sticksstones12a  42411  sticksstones12  42412  rhmpsr  42805  selvvvval  42828  fsuppind  42833  dgrsub2  43377  reabssgn  43877  dirkerval  46335  fourierdlem111  46461  fourierdlem112  46462  fourierdlem113  46463  hsphoif  46820  hsphoival  46823  hoidmvlelem5  46843  hoidifhspval2  46859  hspmbllem2  46871  itcoval  48907