Theorem ifeq12d 4486

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

Syntax hints:   → wi 4   = wceq 1533  ifcif 4466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-un 3940  df-if 4467

This theorem is referenced by:  ifbieq12d  4493  csbif  4521  oev  8133  dfac12r  9566  xaddpnf1  12613  swrdccat3blem  14095  relexpsucnnr  14378  ruclem1  15578  eucalgval  15920  gsumpropd  17882  gsumpropd2lem  17883  gsumress  17886  mulgfval  18220  mulgfvalALT  18221  mulgpropd  18263  frgpup3lem  18897  subrgmvr  20236  isobs  20858  uvcfval  20922  matsc  21053  scmatscmide  21110  marrepval0  21164  marepvval0  21169  mulmarep1el  21175  madufval  21240  madugsum  21246  minmar1fval  21249  pmat1opsc  21301  pmat1ovscd  21302  mat2pmat1  21334  decpmatid  21372  idpm2idmp  21403  pcoval  23609  pcorevlem  23624  itg2const  24335  ditgeq3  24442  efrlim  25541  lgsval  25871  rpvmasum2  26082  fzto1st  30740  psgnfzto1st  30742  xrhval  31254  itg2addnclem  34937  ftc1anclem5  34965  hdmap1fval  38926  dgrsub2  39728  dirkerval  42370  fourierdlem111  42496  fourierdlem112  42497  fourierdlem113  42498  hsphoif  42852  hsphoival  42855  hoidmvlelem5  42875  hoidifhspval2  42891  hspmbllem2  42903