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 2798	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐶) = if(𝜓, 𝐵, 𝐷))

Syntax hints:   → wi 4   = wceq 1570  ifcif 4488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-un 3911  df-if 4489

This theorem is referenced by:  ifbieq12d  4517  csbif  4546  oev  8500  dfac12r  10131  xaddpnf1  13253  swrdccat3blem  14778  relexpsucnnr  15064  ruclem1  16288  eucalgval  16641  gsumpropd  18737  gsumpropd2lem  18738  gsumress  18741  mulgfval  19136  mulgfvalALT  19137  mulgpropd  19183  frgpup3lem  19848  isobs  21851  uvcfval  21915  psrascl  22109  subrgmvr  22165  selvvvval  22274  psdmvr  22313  rhmmpl  22521  rhmply1vr1  22525  matsc  22588  scmatscmide  22645  marrepval0  22699  marepvval0  22704  mulmarep1el  22710  madufval  22775  madugsum  22781  minmar1fval  22784  pmat1opsc  22837  pmat1ovscd  22838  mat2pmat1  22870  decpmatid  22908  idpm2idmp  22939  pcoval  25151  pcorevlem  25166  itg2const  25880  ditgeq3  25990  efrlim  27115  lgsval  27446  rpvmasum2  27657  expsval  28599  fzto1st  33404  psgnfzto1st  33406  mplasclco  33887  extvval  33902  esplyfval0  33935  xrhval  34389  cbvditgdavw  36775  itg2addnclem  38303  ftc1anclem5  38329  hdmap1fval  42551  sticksstones12a  42905  sticksstones12  42906  rhmpsr  43298  fsuppind  43305  dgrsub2  43845  reabssgn  44345  dirkerval  46788  fourierdlem111  46914  fourierdlem112  46915  fourierdlem113  46916  hsphoif  47273  hsphoival  47276  hoidmvlelem5  47296  hoidifhspval2  47312  hspmbllem2  47324  itcoval  49424