Theorem ifeq12d 4504

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ifcif 4482

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-un 3904  df-if 4483

This theorem is used by:  ifbieq12d  4511  csbif  4540  oev  8506  dfac12r  10206  xaddpnf1  13337  swrdccat3blem  14868  relexpsucnnr  15158  ruclem1  16379  eucalgval  16737  gsumpropd  18847  gsumpropd2lem  18848  gsumress  18851  mulgfval  19259  mulgfvalALT  19260  mulgpropd  19306  frgpup3lem  19971  isobs  22006  uvcfval  22070  psrascl  22266  subrgmvr  22322  selvvvval  22431  psdmvr  22470  rhmmpl  22678  rhmply1vr1  22682  matsc  22745  scmatscmide  22802  marrepval0  22856  marepvval0  22861  mulmarep1el  22867  madufval  22932  madugsum  22938  minmar1fval  22941  pmat1opsc  22997  pmat1ovscd  22998  mat2pmat1  23030  decpmatid  23068  idpm2idmp  23099  pcoval  25312  pcorevlem  25327  itg2const  26041  ditgeq3  26150  efrlim  27279  lgsval  27610  rpvmasum2  27821  expsval  28793  fzto1st  33646  psgnfzto1st  33648  mplasclco  34130  extvval  34145  esplyfval0  34178  xrhval  34632  cbvditgdavw  37041  itg2addnclem  38557  ftc1anclem5  38583  hdmap1fval  42821  sticksstones12a  43175  sticksstones12  43176  rhmpsr  43573  fsuppind  43580  dgrsub2  44095  reabssgn  44595  dirkerval  47045  fourierdlem111  47171  fourierdlem112  47172  fourierdlem113  47173  hsphoif  47530  hsphoival  47533  hoidmvlelem5  47553  hoidifhspval2  47569  hspmbllem2  47581  itcoval  49717  crosspval  50898  veronesematrowexpd  50926