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 2858	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐷))

Syntax hints:   → wi 4   = wceq 1537  ifcif 4469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-un 3943  df-if 4470

This theorem is referenced by:  ifbieq12d  4496  csbif  4524  oev  8141  dfac12r  9574  xaddpnf1  12622  swrdccat3blem  14103  relexpsucnnr  14386  ruclem1  15586  eucalgval  15928  gsumpropd  17890  gsumpropd2lem  17891  gsumress  17894  mulgfval  18228  mulgfvalALT  18229  mulgpropd  18271  frgpup3lem  18905  subrgmvr  20244  isobs  20866  uvcfval  20930  matsc  21061  scmatscmide  21118  marrepval0  21172  marepvval0  21177  mulmarep1el  21183  madufval  21248  madugsum  21254  minmar1fval  21257  pmat1opsc  21309  pmat1ovscd  21310  mat2pmat1  21342  decpmatid  21380  idpm2idmp  21411  pcoval  23617  pcorevlem  23632  itg2const  24343  ditgeq3  24450  efrlim  25549  lgsval  25879  rpvmasum2  26090  fzto1st  30747  psgnfzto1st  30749  xrhval  31261  itg2addnclem  34945  ftc1anclem5  34973  hdmap1fval  38934  dgrsub2  39742  dirkerval  42383  fourierdlem111  42509  fourierdlem112  42510  fourierdlem113  42511  hsphoif  42865  hsphoival  42868  hoidmvlelem5  42888  hoidifhspval2  42904  hspmbllem2  42916