Theorem ifeq12d 4056

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

Syntax hints:   → wi 4   = wceq 1475  ifcif 4036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-un 3545  df-if 4037

This theorem is referenced by:  ifbieq12d  4063  csbif  4088  oev  7481  dfac12r  8851  xaddpnf1  11931  swrdccat3blem  13346  relexpsucnnr  13613  ruclem1  14799  eucalgval  15133  gsumpropd  17095  gsumpropd2lem  17096  gsumress  17099  mulgfval  17365  mulgpropd  17407  frgpup3lem  18013  subrgmvr  19282  isobs  19883  uvcfval  19942  matsc  20075  scmatscmide  20132  marrepval0  20186  marepvval0  20191  mulmarep1el  20197  madufval  20262  madugsum  20268  minmar1fval  20271  pmat1opsc  20323  pmat1ovscd  20324  mat2pmat1  20356  decpmatid  20394  idpm2idmp  20425  pcoval  22619  pcorevlem  22634  itg2const  23313  ditgeq3  23420  efrlim  24496  lgsval  24826  rpvmasum2  25001  fzto1st  29184  psgnfzto1st  29186  xrhval  29390  itg2addnclem  32631  ftc1anclem5  32659  hdmap1fval  36104  dgrsub2  36724  dirkerval  38984  fourierdlem111  39110  fourierdlem112  39111  fourierdlem113  39112  hsphoif  39466  hsphoival  39469  hoidmvlelem5  39489  hoidifhspval2  39505  hspmbllem2  39517