Theorem ifeq12d 4546

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

Syntax hints:   → wi 4   = wceq 1539  ifcif 4524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-un 3955  df-if 4525

This theorem is referenced by:  ifbieq12d  4553  csbif  4582  oev  8553  dfac12r  10188  xaddpnf1  13269  swrdccat3blem  14778  relexpsucnnr  15065  ruclem1  16268  eucalgval  16620  gsumpropd  18692  gsumpropd2lem  18693  gsumress  18696  mulgfval  19088  mulgfvalALT  19089  mulgpropd  19135  frgpup3lem  19796  isobs  21741  uvcfval  21805  psrascl  22000  subrgmvr  22052  psdmvr  22174  rhmmpl  22388  rhmply1vr1  22392  matsc  22457  scmatscmide  22514  marrepval0  22568  marepvval0  22573  mulmarep1el  22579  madufval  22644  madugsum  22650  minmar1fval  22653  pmat1opsc  22706  pmat1ovscd  22707  mat2pmat1  22739  decpmatid  22777  idpm2idmp  22808  pcoval  25045  pcorevlem  25060  itg2const  25776  ditgeq3  25886  efrlim  27013  efrlimOLD  27014  lgsval  27346  rpvmasum2  27557  expsval  28409  fzto1st  33124  psgnfzto1st  33126  xrhval  34020  cbvditgdavw  36284  itg2addnclem  37679  ftc1anclem5  37705  hdmap1fval  41799  sticksstones12a  42159  sticksstones12  42160  rhmpsr  42567  selvvvval  42600  fsuppind  42605  dgrsub2  43152  reabssgn  43654  dirkerval  46111  fourierdlem111  46237  fourierdlem112  46238  fourierdlem113  46239  hsphoif  46596  hsphoival  46599  hoidmvlelem5  46619  hoidifhspval2  46635  hspmbllem2  46647  itcoval  48587