Theorem ifeq12d 4488

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

Syntax hints:   → wi 4   = wceq 1542  ifcif 4466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-un 3894  df-if 4467

This theorem is referenced by:  ifbieq12d  4495  csbif  4524  oev  8449  dfac12r  10069  xaddpnf1  13178  swrdccat3blem  14701  relexpsucnnr  14987  ruclem1  16198  eucalgval  16551  gsumpropd  18646  gsumpropd2lem  18647  gsumress  18650  mulgfval  19045  mulgfvalALT  19046  mulgpropd  19092  frgpup3lem  19752  isobs  21700  uvcfval  21764  psrascl  21957  subrgmvr  22011  psdmvr  22135  rhmmpl  22348  rhmply1vr1  22352  matsc  22415  scmatscmide  22472  marrepval0  22526  marepvval0  22531  mulmarep1el  22537  madufval  22602  madugsum  22608  minmar1fval  22611  pmat1opsc  22664  pmat1ovscd  22665  mat2pmat1  22697  decpmatid  22735  idpm2idmp  22766  pcoval  24978  pcorevlem  24993  itg2const  25707  ditgeq3  25817  efrlim  26933  lgsval  27264  rpvmasum2  27475  expsval  28417  fzto1st  33164  psgnfzto1st  33166  extvval  33675  esplyfval0  33708  xrhval  34162  cbvditgdavw  36464  itg2addnclem  37992  ftc1anclem5  38018  hdmap1fval  42242  sticksstones12a  42596  sticksstones12  42597  rhmpsr  42995  selvvvval  43018  fsuppind  43023  dgrsub2  43563  reabssgn  44063  dirkerval  46519  fourierdlem111  46645  fourierdlem112  46646  fourierdlem113  46647  hsphoif  47004  hsphoival  47007  hoidmvlelem5  47027  hoidifhspval2  47043  hspmbllem2  47055  itcoval  49137