Theorem ifeq12d 4497

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

Syntax hints:   → wi 4   = wceq 1541  ifcif 4475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-un 3907  df-if 4476

This theorem is referenced by:  ifbieq12d  4504  csbif  4533  oev  8429  dfac12r  10038  xaddpnf1  13125  swrdccat3blem  14646  relexpsucnnr  14932  ruclem1  16140  eucalgval  16493  gsumpropd  18586  gsumpropd2lem  18587  gsumress  18590  mulgfval  18982  mulgfvalALT  18983  mulgpropd  19029  frgpup3lem  19690  isobs  21658  uvcfval  21722  psrascl  21917  subrgmvr  21969  psdmvr  22085  rhmmpl  22299  rhmply1vr1  22303  matsc  22366  scmatscmide  22423  marrepval0  22477  marepvval0  22482  mulmarep1el  22488  madufval  22553  madugsum  22559  minmar1fval  22562  pmat1opsc  22615  pmat1ovscd  22616  mat2pmat1  22648  decpmatid  22686  idpm2idmp  22717  pcoval  24939  pcorevlem  24954  itg2const  25669  ditgeq3  25779  efrlim  26907  efrlimOLD  26908  lgsval  27240  rpvmasum2  27451  expsval  28349  fzto1st  33070  psgnfzto1st  33072  xrhval  34029  cbvditgdavw  36322  itg2addnclem  37717  ftc1anclem5  37743  hdmap1fval  41841  sticksstones12a  42196  sticksstones12  42197  rhmpsr  42591  selvvvval  42624  fsuppind  42629  dgrsub2  43174  reabssgn  43675  dirkerval  46135  fourierdlem111  46261  fourierdlem112  46262  fourierdlem113  46263  hsphoif  46620  hsphoival  46623  hoidmvlelem5  46643  hoidifhspval2  46659  hspmbllem2  46671  itcoval  48699