Theorem ifeq12d 4480

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

Syntax hints:   → wi 4   = wceq 1539  ifcif 4459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-un 3892  df-if 4460

This theorem is referenced by:  ifbieq12d  4487  csbif  4516  oev  8344  dfac12r  9902  xaddpnf1  12960  swrdccat3blem  14452  relexpsucnnr  14736  ruclem1  15940  eucalgval  16287  gsumpropd  18362  gsumpropd2lem  18363  gsumress  18366  mulgfval  18702  mulgfvalALT  18703  mulgpropd  18745  frgpup3lem  19383  isobs  20927  uvcfval  20991  subrgmvr  21234  matsc  21599  scmatscmide  21656  marrepval0  21710  marepvval0  21715  mulmarep1el  21721  madufval  21786  madugsum  21792  minmar1fval  21795  pmat1opsc  21848  pmat1ovscd  21849  mat2pmat1  21881  decpmatid  21919  idpm2idmp  21950  pcoval  24174  pcorevlem  24189  itg2const  24905  ditgeq3  25014  efrlim  26119  lgsval  26449  rpvmasum2  26660  fzto1st  31370  psgnfzto1st  31372  xrhval  31968  itg2addnclem  35828  ftc1anclem5  35854  hdmap1fval  39810  sticksstones12a  40113  sticksstones12  40114  fsuppind  40279  mhphf  40285  dgrsub2  40960  reabssgn  41244  dirkerval  43632  fourierdlem111  43758  fourierdlem112  43759  fourierdlem113  43760  hsphoif  44114  hsphoival  44117  hoidmvlelem5  44137  hoidifhspval2  44153  hspmbllem2  44165  itcoval  46007