Theorem ifeq12d 4510

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

Syntax hints:   → wi 4   = wceq 1540  ifcif 4488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-un 3919  df-if 4489

This theorem is referenced by:  ifbieq12d  4517  csbif  4546  oev  8478  dfac12r  10100  xaddpnf1  13186  swrdccat3blem  14704  relexpsucnnr  14991  ruclem1  16199  eucalgval  16552  gsumpropd  18605  gsumpropd2lem  18606  gsumress  18609  mulgfval  19001  mulgfvalALT  19002  mulgpropd  19048  frgpup3lem  19707  isobs  21629  uvcfval  21693  psrascl  21888  subrgmvr  21940  psdmvr  22056  rhmmpl  22270  rhmply1vr1  22274  matsc  22337  scmatscmide  22394  marrepval0  22448  marepvval0  22453  mulmarep1el  22459  madufval  22524  madugsum  22530  minmar1fval  22533  pmat1opsc  22586  pmat1ovscd  22587  mat2pmat1  22619  decpmatid  22657  idpm2idmp  22688  pcoval  24911  pcorevlem  24926  itg2const  25641  ditgeq3  25751  efrlim  26879  efrlimOLD  26880  lgsval  27212  rpvmasum2  27423  expsval  28311  fzto1st  33060  psgnfzto1st  33062  xrhval  34008  cbvditgdavw  36270  itg2addnclem  37665  ftc1anclem5  37691  hdmap1fval  41790  sticksstones12a  42145  sticksstones12  42146  rhmpsr  42540  selvvvval  42573  fsuppind  42578  dgrsub2  43124  reabssgn  43625  dirkerval  46089  fourierdlem111  46215  fourierdlem112  46216  fourierdlem113  46217  hsphoif  46574  hsphoival  46577  hoidmvlelem5  46597  hoidifhspval2  46613  hspmbllem2  46625  itcoval  48650