Theorem ifeqda 4514

Description: Separation of the values of the conditional operator. (Contributed by Alexander van der Vekens, 13-Apr-2018.)

Hypotheses

Ref	Expression
ifeqda.1	⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
ifeqda.2	⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶)

Assertion

Ref	Expression
ifeqda	⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶)

Proof of Theorem ifeqda

Step	Hyp	Ref	Expression
1		iftrue 4483	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 485	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifeqda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
4	2, 3	eqtrd 2796	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
5		iffalse 4486	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 485	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifeqda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶)
8	6, 7	eqtrd 2796	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
9	4, 8	pm2.61dan 822	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1559  ifcif 4477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4478

This theorem is referenced by:  somincom  6117  cantnfp1  9630  ccatsymb  14590  swrdccat3blem  14746  repswccat  14793  ccatco  14842  bitsinvp1  16474  xrsdsreval  21452  fvmptnn04if  22897  chfacfscmulgsum  22908  chfacfpmmulgsum  22912  oprpiece1res2  25002  phtpycc  25041  plymulidp  26334  atantayl2  26991  ifeq3da  32705  fprodex01  32988  psgnfzto1stlem  33241  fzto1st1  33243  cycpm2tr  33260  elrgspnlem4  33387  elrspunsn  33576  esplyfval1  33831  esplyind  33833  fldextrspunlsp  33932  mdetlap1  34084  madjusmdetlem1  34085  madjusmdetlem2  34086  ccatmulgnn0dir  34800  itgexpif  34861  repr0  34866  elmrsubrn  35831  matunitlindflem1  38076  sticksstones12  42736  redvmptabs  42930  readvrec  42932  frlmvscadiccat  43089  fsuppind  43133  fsuppssindlem1  43134  reabsifneg  44169  reabsifnpos  44170  reabsifpos  44171  reabsifnneg  44172  reabssgn  44173  sqrtcval  44178  mnringmulrcld  44765  fourierdlem101  46742  hoidmv1lelem2  47127  dfafv2  47687  m1modmmod  47919  indprm  48199  indprmfz  48200  linc0scn0  49006  digexp  49190