Theorem ifeq12d 4248

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

Syntax hints:   → wi 4   = wceq 1630  ifcif 4228

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-rab 3057  df-v 3340  df-un 3718  df-if 4229

This theorem is referenced by:  ifbieq12d  4255  csbif  4280  oev  7761  dfac12r  9158  xaddpnf1  12248  swrdccat3blem  13693  relexpsucnnr  13962  ruclem1  15157  eucalgval  15495  gsumpropd  17471  gsumpropd2lem  17472  gsumress  17475  mulgfval  17741  mulgpropd  17783  frgpup3lem  18388  subrgmvr  19661  isobs  20264  uvcfval  20323  matsc  20456  scmatscmide  20513  marrepval0  20567  marepvval0  20572  mulmarep1el  20578  madufval  20643  madugsum  20649  minmar1fval  20652  pmat1opsc  20704  pmat1ovscd  20705  mat2pmat1  20737  decpmatid  20775  idpm2idmp  20806  pcoval  23009  pcorevlem  23024  itg2const  23704  ditgeq3  23811  efrlim  24893  lgsval  25223  rpvmasum2  25398  fzto1st  30160  psgnfzto1st  30162  xrhval  30369  itg2addnclem  33772  ftc1anclem5  33800  hdmap1fval  37586  dgrsub2  38205  dirkerval  40809  fourierdlem111  40935  fourierdlem112  40936  fourierdlem113  40937  hsphoif  41294  hsphoival  41297  hoidmvlelem5  41317  hoidifhspval2  41333  hspmbllem2  41345