Theorem ifeq12d 4505

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

Syntax hints:   → wi 4   = wceq 1563  ifcif 4483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-un 3912  df-if 4484

This theorem is referenced by:  ifbieq12d  4512  csbif  4541  oev  8487  dfac12r  10118  xaddpnf1  13240  swrdccat3blem  14764  relexpsucnnr  15050  ruclem1  16275  eucalgval  16628  gsumpropd  18724  gsumpropd2lem  18725  gsumress  18728  mulgfval  19123  mulgfvalALT  19124  mulgpropd  19170  frgpup3lem  19835  isobs  21827  uvcfval  21891  psrascl  22085  subrgmvr  22141  selvvvval  22250  psdmvr  22289  rhmmpl  22497  rhmply1vr1  22501  matsc  22564  scmatscmide  22621  marrepval0  22675  marepvval0  22680  mulmarep1el  22686  madufval  22751  madugsum  22757  minmar1fval  22760  pmat1opsc  22813  pmat1ovscd  22814  mat2pmat1  22846  decpmatid  22884  idpm2idmp  22915  pcoval  25127  pcorevlem  25142  itg2const  25856  ditgeq3  25966  efrlim  27088  lgsval  27419  rpvmasum2  27630  expsval  28572  fzto1st  33331  psgnfzto1st  33333  mplasclco  33818  extvval  33833  esplyfval0  33866  xrhval  34320  cbvditgdavw  36650  itg2addnclem  38177  ftc1anclem5  38203  hdmap1fval  42427  sticksstones12a  42781  sticksstones12  42782  rhmpsr  43172  fsuppind  43179  dgrsub2  43719  reabssgn  44219  dirkerval  46664  fourierdlem111  46790  fourierdlem112  46791  fourierdlem113  46792  hsphoif  47149  hsphoival  47152  hoidmvlelem5  47172  hoidifhspval2  47188  hspmbllem2  47200  itcoval  49293