Theorem ifeq12d 4552

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

Syntax hints:   → wi 4   = wceq 1537  ifcif 4531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-un 3968  df-if 4532

This theorem is referenced by:  ifbieq12d  4559  csbif  4588  oev  8551  dfac12r  10185  xaddpnf1  13265  swrdccat3blem  14774  relexpsucnnr  15061  ruclem1  16264  eucalgval  16616  gsumpropd  18704  gsumpropd2lem  18705  gsumress  18708  mulgfval  19100  mulgfvalALT  19101  mulgpropd  19147  frgpup3lem  19810  isobs  21758  uvcfval  21822  psrascl  22017  subrgmvr  22069  rhmmpl  22403  rhmply1vr1  22407  matsc  22472  scmatscmide  22529  marrepval0  22583  marepvval0  22588  mulmarep1el  22594  madufval  22659  madugsum  22665  minmar1fval  22668  pmat1opsc  22721  pmat1ovscd  22722  mat2pmat1  22754  decpmatid  22792  idpm2idmp  22823  pcoval  25058  pcorevlem  25073  itg2const  25790  ditgeq3  25900  efrlim  27027  efrlimOLD  27028  lgsval  27360  rpvmasum2  27571  expsval  28423  fzto1st  33106  psgnfzto1st  33108  xrhval  33981  cbvditgdavw  36265  itg2addnclem  37658  ftc1anclem5  37684  hdmap1fval  41779  sticksstones12a  42139  sticksstones12  42140  rhmpsr  42539  selvvvval  42572  fsuppind  42577  dgrsub2  43124  reabssgn  43626  dirkerval  46047  fourierdlem111  46173  fourierdlem112  46174  fourierdlem113  46175  hsphoif  46532  hsphoival  46535  hoidmvlelem5  46555  hoidifhspval2  46571  hspmbllem2  46583  itcoval  48511