Theorem ifeq12d 4569

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

Syntax hints:   → wi 4   = wceq 1537  ifcif 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-un 3981  df-if 4549

This theorem is referenced by:  ifbieq12d  4576  csbif  4605  oev  8570  dfac12r  10216  xaddpnf1  13288  swrdccat3blem  14787  relexpsucnnr  15074  ruclem1  16279  eucalgval  16629  gsumpropd  18716  gsumpropd2lem  18717  gsumress  18720  mulgfval  19109  mulgfvalALT  19110  mulgpropd  19156  frgpup3lem  19819  isobs  21763  uvcfval  21827  psrascl  22022  subrgmvr  22074  rhmmpl  22408  rhmply1vr1  22412  matsc  22477  scmatscmide  22534  marrepval0  22588  marepvval0  22593  mulmarep1el  22599  madufval  22664  madugsum  22670  minmar1fval  22673  pmat1opsc  22726  pmat1ovscd  22727  mat2pmat1  22759  decpmatid  22797  idpm2idmp  22828  pcoval  25063  pcorevlem  25078  itg2const  25795  ditgeq3  25905  efrlim  27030  efrlimOLD  27031  lgsval  27363  rpvmasum2  27574  expsval  28426  fzto1st  33096  psgnfzto1st  33098  xrhval  33964  cbvditgdavw  36248  itg2addnclem  37631  ftc1anclem5  37657  hdmap1fval  41753  sticksstones12a  42114  sticksstones12  42115  rhmpsr  42507  selvvvval  42540  fsuppind  42545  dgrsub2  43092  reabssgn  43598  dirkerval  46012  fourierdlem111  46138  fourierdlem112  46139  fourierdlem113  46140  hsphoif  46497  hsphoival  46500  hoidmvlelem5  46520  hoidifhspval2  46536  hspmbllem2  46548  itcoval  48395