Theorem ifeq12d 4078

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

Syntax hints:   → wi 4   = wceq 1480  ifcif 4058

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2916  df-v 3188  df-un 3560  df-if 4059

This theorem is referenced by:  ifbieq12d  4085  csbif  4110  oev  7539  dfac12r  8912  xaddpnf1  12000  swrdccat3blem  13432  relexpsucnnr  13699  ruclem1  14885  eucalgval  15219  gsumpropd  17193  gsumpropd2lem  17194  gsumress  17197  mulgfval  17463  mulgpropd  17505  frgpup3lem  18111  subrgmvr  19380  isobs  19983  uvcfval  20042  matsc  20175  scmatscmide  20232  marrepval0  20286  marepvval0  20291  mulmarep1el  20297  madufval  20362  madugsum  20368  minmar1fval  20371  pmat1opsc  20423  pmat1ovscd  20424  mat2pmat1  20456  decpmatid  20494  idpm2idmp  20525  pcoval  22719  pcorevlem  22734  itg2const  23413  ditgeq3  23520  efrlim  24596  lgsval  24926  rpvmasum2  25101  fzto1st  29635  psgnfzto1st  29637  xrhval  29841  itg2addnclem  33090  ftc1anclem5  33118  hdmap1fval  36563  dgrsub2  37183  dirkerval  39612  fourierdlem111  39738  fourierdlem112  39739  fourierdlem113  39740  hsphoif  40094  hsphoival  40097  hoidmvlelem5  40117  hoidifhspval2  40133  hspmbllem2  40145