Theorem ifeq12d 4527

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

Syntax hints:   → wi 4   = wceq 1539  ifcif 4505

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 2706

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 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-v 3465  df-un 3936  df-if 4506

This theorem is referenced by:  ifbieq12d  4534  csbif  4563  oev  8534  dfac12r  10169  xaddpnf1  13250  swrdccat3blem  14759  relexpsucnnr  15046  ruclem1  16249  eucalgval  16601  gsumpropd  18660  gsumpropd2lem  18661  gsumress  18664  mulgfval  19056  mulgfvalALT  19057  mulgpropd  19103  frgpup3lem  19763  isobs  21694  uvcfval  21758  psrascl  21953  subrgmvr  22005  psdmvr  22121  rhmmpl  22335  rhmply1vr1  22339  matsc  22404  scmatscmide  22461  marrepval0  22515  marepvval0  22520  mulmarep1el  22526  madufval  22591  madugsum  22597  minmar1fval  22600  pmat1opsc  22653  pmat1ovscd  22654  mat2pmat1  22686  decpmatid  22724  idpm2idmp  22755  pcoval  24980  pcorevlem  24995  itg2const  25711  ditgeq3  25821  efrlim  26948  efrlimOLD  26949  lgsval  27281  rpvmasum2  27492  expsval  28344  fzto1st  33062  psgnfzto1st  33064  xrhval  33978  cbvditgdavw  36242  itg2addnclem  37637  ftc1anclem5  37663  hdmap1fval  41757  sticksstones12a  42117  sticksstones12  42118  rhmpsr  42525  selvvvval  42558  fsuppind  42563  dgrsub2  43110  reabssgn  43611  dirkerval  46063  fourierdlem111  46189  fourierdlem112  46190  fourierdlem113  46191  hsphoif  46548  hsphoival  46551  hoidmvlelem5  46571  hoidifhspval2  46587  hspmbllem2  46599  itcoval  48540