Theorem ifeq12d 4483

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

Syntax hints:   → wi 4   = wceq 1547  ifcif 4461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-un 3895  df-if 4462

This theorem is referenced by:  ifbieq12d  4490  csbif  4519  oev  8446  dfac12r  10067  xaddpnf1  13176  swrdccat3blem  14699  relexpsucnnr  14985  ruclem1  16196  eucalgval  16549  gsumpropd  18644  gsumpropd2lem  18645  gsumress  18648  mulgfval  19043  mulgfvalALT  19044  mulgpropd  19090  frgpup3lem  19750  isobs  21702  uvcfval  21766  psrascl  21960  subrgmvr  22016  selvvvval  22125  psdmvr  22164  rhmmpl  22373  rhmply1vr1  22377  matsc  22440  scmatscmide  22497  marrepval0  22551  marepvval0  22556  mulmarep1el  22562  madufval  22627  madugsum  22633  minmar1fval  22636  pmat1opsc  22689  pmat1ovscd  22690  mat2pmat1  22722  decpmatid  22760  idpm2idmp  22791  pcoval  25003  pcorevlem  25018  itg2const  25732  ditgeq3  25842  efrlim  26958  lgsval  27289  rpvmasum2  27500  expsval  28442  fzto1st  33191  psgnfzto1st  33193  mplasclco  33707  extvval  33722  esplyfval0  33755  xrhval  34209  cbvditgdavw  36517  itg2addnclem  38045  ftc1anclem5  38071  hdmap1fval  42295  sticksstones12a  42649  sticksstones12  42650  rhmpsr  43040  fsuppind  43047  dgrsub2  43587  reabssgn  44087  dirkerval  46541  fourierdlem111  46667  fourierdlem112  46668  fourierdlem113  46669  hsphoif  47026  hsphoival  47029  hoidmvlelem5  47049  hoidifhspval2  47065  hspmbllem2  47077  itcoval  49159