Theorem ifeq12d 4507

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ifcif 4485

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-un 4154  df-if 4486

This theorem is used by:  ifbieq12d  4514  csbif  4543  oev  8553  dfac12r  10255  xaddpnf1  13386  swrdccat3blem  14919  relexpsucnnr  15210  ruclem1  16431  eucalgval  16789  gsumpropd  18899  gsumpropd2lem  18900  gsumress  18903  mulgfval  19311  mulgfvalALT  19312  mulgpropd  19358  frgpup3lem  20024  isobs  22059  uvcfval  22123  psrascl  22319  subrgmvr  22375  selvvvval  22484  psdmvr  22523  rhmmpl  22731  rhmply1vr1  22735  matsc  22798  scmatscmide  22855  marrepval0  22909  marepvval0  22914  mulmarep1el  22920  madufval  22985  madugsum  22991  minmar1fval  22994  pmat1opsc  23050  pmat1ovscd  23051  mat2pmat1  23083  decpmatid  23121  idpm2idmp  23152  pcoval  25365  pcorevlem  25380  itg2const  26094  ditgeq3  26203  efrlim  27330  lgsval  27661  rpvmasum2  27872  expsval  28844  fzto1st  33740  psgnfzto1st  33742  mplasclco  34231  extvval  34246  esplyfval0  34279  xrhval  34733  cbvditgdavw  37262  itg2addnclem  38794  ftc1anclem5  38820  hdmap1fval  43056  sticksstones12a  43410  sticksstones12  43411  rhmpsr  43815  fsuppind  43822  dgrsub2  44340  reabssgn  44839  dirkerval  47316  fourierdlem111  47442  fourierdlem112  47443  fourierdlem113  47444  hsphoif  47801  hsphoival  47804  hoidmvlelem5  47824  hoidifhspval2  47840  hspmbllem2  47852  itcoval  49988  crosspval  51266  veronesematrowexpd  51294