Theorem ifeq12d 4477

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

Syntax hints:   → wi 4   = wceq 1539  ifcif 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-un 3888  df-if 4457

This theorem is referenced by:  ifbieq12d  4484  csbif  4513  oev  8306  dfac12r  9833  xaddpnf1  12889  swrdccat3blem  14380  relexpsucnnr  14664  ruclem1  15868  eucalgval  16215  gsumpropd  18277  gsumpropd2lem  18278  gsumress  18281  mulgfval  18617  mulgfvalALT  18618  mulgpropd  18660  frgpup3lem  19298  isobs  20837  uvcfval  20901  subrgmvr  21144  matsc  21507  scmatscmide  21564  marrepval0  21618  marepvval0  21623  mulmarep1el  21629  madufval  21694  madugsum  21700  minmar1fval  21703  pmat1opsc  21756  pmat1ovscd  21757  mat2pmat1  21789  decpmatid  21827  idpm2idmp  21858  pcoval  24080  pcorevlem  24095  itg2const  24810  ditgeq3  24919  efrlim  26024  lgsval  26354  rpvmasum2  26565  fzto1st  31272  psgnfzto1st  31274  xrhval  31868  itg2addnclem  35755  ftc1anclem5  35781  hdmap1fval  39737  sticksstones12a  40041  sticksstones12  40042  fsuppind  40202  mhphf  40208  dgrsub2  40876  reabssgn  41133  dirkerval  43522  fourierdlem111  43648  fourierdlem112  43649  fourierdlem113  43650  hsphoif  44004  hsphoival  44007  hoidmvlelem5  44027  hoidifhspval2  44043  hspmbllem2  44055  itcoval  45895