Theorem ifeq12d 4549

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

Syntax hints:   → wi 4   = wceq 1540  ifcif 4528

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-un 3953  df-if 4529

This theorem is referenced by:  ifbieq12d  4556  csbif  4585  oev  8520  dfac12r  10147  xaddpnf1  13212  swrdccat3blem  14696  relexpsucnnr  14979  ruclem1  16181  eucalgval  16526  gsumpropd  18609  gsumpropd2lem  18610  gsumress  18613  mulgfval  18995  mulgfvalALT  18996  mulgpropd  19039  frgpup3lem  19693  isobs  21585  uvcfval  21649  subrgmvr  21899  matsc  22272  scmatscmide  22329  marrepval0  22383  marepvval0  22388  mulmarep1el  22394  madufval  22459  madugsum  22465  minmar1fval  22468  pmat1opsc  22521  pmat1ovscd  22522  mat2pmat1  22554  decpmatid  22592  idpm2idmp  22623  pcoval  24858  pcorevlem  24873  itg2const  25590  ditgeq3  25699  efrlim  26815  lgsval  27147  rpvmasum2  27358  fzto1st  32698  psgnfzto1st  32700  xrhval  33462  itg2addnclem  37003  ftc1anclem5  37029  hdmap1fval  41131  sticksstones12a  41440  sticksstones12  41441  rhmmpl  41588  selvvvval  41620  fsuppind  41625  dgrsub2  42340  reabssgn  42850  dirkerval  45266  fourierdlem111  45392  fourierdlem112  45393  fourierdlem113  45394  hsphoif  45751  hsphoival  45754  hoidmvlelem5  45774  hoidifhspval2  45790  hspmbllem2  45802  itcoval  47509