Theorem ifeq12d 4489

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

Syntax hints:   → wi 4   = wceq 1542  ifcif 4467

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-un 3895  df-if 4468

This theorem is referenced by:  ifbieq12d  4496  csbif  4525  oev  8442  dfac12r  10060  xaddpnf1  13169  swrdccat3blem  14692  relexpsucnnr  14978  ruclem1  16189  eucalgval  16542  gsumpropd  18637  gsumpropd2lem  18638  gsumress  18641  mulgfval  19036  mulgfvalALT  19037  mulgpropd  19083  frgpup3lem  19743  isobs  21710  uvcfval  21774  psrascl  21967  subrgmvr  22021  psdmvr  22145  rhmmpl  22358  rhmply1vr1  22362  matsc  22425  scmatscmide  22482  marrepval0  22536  marepvval0  22541  mulmarep1el  22547  madufval  22612  madugsum  22618  minmar1fval  22621  pmat1opsc  22674  pmat1ovscd  22675  mat2pmat1  22707  decpmatid  22745  idpm2idmp  22776  pcoval  24988  pcorevlem  25003  itg2const  25717  ditgeq3  25827  efrlim  26946  efrlimOLD  26947  lgsval  27278  rpvmasum2  27489  expsval  28431  fzto1st  33179  psgnfzto1st  33181  extvval  33690  esplyfval0  33723  xrhval  34178  cbvditgdavw  36480  itg2addnclem  38006  ftc1anclem5  38032  hdmap1fval  42256  sticksstones12a  42610  sticksstones12  42611  rhmpsr  43009  selvvvval  43032  fsuppind  43037  dgrsub2  43581  reabssgn  44081  dirkerval  46537  fourierdlem111  46663  fourierdlem112  46664  fourierdlem113  46665  hsphoif  47022  hsphoival  47025  hoidmvlelem5  47045  hoidifhspval2  47061  hspmbllem2  47073  itcoval  49149