Theorem ifeq12d 4139

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

Syntax hints:   → wi 4   = wceq 1523  ifcif 4119

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-un 3612  df-if 4120

This theorem is referenced by:  ifbieq12d  4146  csbif  4171  oev  7639  dfac12r  9006  xaddpnf1  12095  swrdccat3blem  13541  relexpsucnnr  13809  ruclem1  15004  eucalgval  15342  gsumpropd  17319  gsumpropd2lem  17320  gsumress  17323  mulgfval  17589  mulgpropd  17631  frgpup3lem  18236  subrgmvr  19509  isobs  20112  uvcfval  20171  matsc  20304  scmatscmide  20361  marrepval0  20415  marepvval0  20420  mulmarep1el  20426  madufval  20491  madugsum  20497  minmar1fval  20500  pmat1opsc  20552  pmat1ovscd  20553  mat2pmat1  20585  decpmatid  20623  idpm2idmp  20654  pcoval  22857  pcorevlem  22872  itg2const  23552  ditgeq3  23659  efrlim  24741  lgsval  25071  rpvmasum2  25246  fzto1st  29981  psgnfzto1st  29983  xrhval  30190  itg2addnclem  33591  ftc1anclem5  33619  hdmap1fval  37403  dgrsub2  38022  dirkerval  40626  fourierdlem111  40752  fourierdlem112  40753  fourierdlem113  40754  hsphoif  41111  hsphoival  41114  hoidmvlelem5  41134  hoidifhspval2  41150  hspmbllem2  41162