Theorem ifeq12d 4492

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

Syntax hints:   → wi 4   = wceq 1550  ifcif 4470

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-tru 1553  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-rab 3405  df-v 3446  df-un 3900  df-if 4471

This theorem is referenced by:  ifbieq12d  4499  csbif  4528  oev  8467  dfac12r  10089  xaddpnf1  13215  swrdccat3blem  14738  relexpsucnnr  15024  ruclem1  16235  eucalgval  16588  gsumpropd  18684  gsumpropd2lem  18685  gsumress  18688  mulgfval  19083  mulgfvalALT  19084  mulgpropd  19130  frgpup3lem  19789  isobs  21741  uvcfval  21805  psrascl  21999  subrgmvr  22055  selvvvval  22164  psdmvr  22203  rhmmpl  22412  rhmply1vr1  22416  matsc  22479  scmatscmide  22536  marrepval0  22590  marepvval0  22595  mulmarep1el  22601  madufval  22666  madugsum  22672  minmar1fval  22675  pmat1opsc  22728  pmat1ovscd  22729  mat2pmat1  22761  decpmatid  22799  idpm2idmp  22830  pcoval  25042  pcorevlem  25057  itg2const  25771  ditgeq3  25881  efrlim  27000  lgsval  27331  rpvmasum2  27542  expsval  28484  fzto1st  33233  psgnfzto1st  33235  mplasclco  33757  extvval  33772  esplyfval0  33805  xrhval  34259  cbvditgdavw  36580  itg2addnclem  38108  ftc1anclem5  38134  hdmap1fval  42358  sticksstones12a  42712  sticksstones12  42713  rhmpsr  43103  fsuppind  43110  dgrsub2  43650  reabssgn  44150  dirkerval  46603  fourierdlem111  46729  fourierdlem112  46730  fourierdlem113  46731  hsphoif  47088  hsphoival  47091  hoidmvlelem5  47111  hoidifhspval2  47127  hspmbllem2  47139  itcoval  49221