Theorem ifeq12d 4445

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

Syntax hints:   → wi 4   = wceq 1538  ifcif 4425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115  df-v 3443  df-un 3886  df-if 4426

This theorem is referenced by:  ifbieq12d  4452  csbif  4480  oev  8122  dfac12r  9557  xaddpnf1  12607  swrdccat3blem  14092  relexpsucnnr  14376  ruclem1  15576  eucalgval  15916  gsumpropd  17880  gsumpropd2lem  17881  gsumress  17884  mulgfval  18218  mulgfvalALT  18219  mulgpropd  18261  frgpup3lem  18895  isobs  20409  uvcfval  20473  subrgmvr  20701  matsc  21055  scmatscmide  21112  marrepval0  21166  marepvval0  21171  mulmarep1el  21177  madufval  21242  madugsum  21248  minmar1fval  21251  pmat1opsc  21304  pmat1ovscd  21305  mat2pmat1  21337  decpmatid  21375  idpm2idmp  21406  pcoval  23616  pcorevlem  23631  itg2const  24344  ditgeq3  24453  efrlim  25555  lgsval  25885  rpvmasum2  26096  fzto1st  30795  psgnfzto1st  30797  xrhval  31369  itg2addnclem  35108  ftc1anclem5  35134  hdmap1fval  39092  fsuppind  39456  dgrsub2  40079  reabssgn  40336  dirkerval  42733  fourierdlem111  42859  fourierdlem112  42860  fourierdlem113  42861  hsphoif  43215  hsphoival  43218  hoidmvlelem5  43238  hoidifhspval2  43254  hspmbllem2  43266  itcoval  45075