Theorem ifeqda 4493

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 4462	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 483	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifeqda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
4	2, 3	eqtrd 2776	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
5		iffalse 4465	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 483	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifeqda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶)
8	6, 7	eqtrd 2776	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
9	4, 8	pm2.61dan 819	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   = wceq 1548  ifcif 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-ex 1788  df-sb 2075  df-clab 2720  df-cleq 2733  df-clel 2816  df-if 4457

This theorem is referenced by:  somincom  6090  cantnfp1  9597  ccatsymb  14540  swrdccat3blem  14696  repswccat  14743  ccatco  14792  bitsinvp1  16413  xrsdsreval  21390  fvmptnn04if  22835  chfacfscmulgsum  22846  chfacfpmmulgsum  22850  oprpiece1res2  24940  phtpycc  24979  atantayl2  26923  ifeq3da  32636  fprodex01  32919  psgnfzto1stlem  33183  fzto1st1  33185  cycpm2tr  33202  elrgspnlem4  33328  elrspunsn  33514  esplyfval1  33767  esplyind  33769  fldextrspunlsp  33868  mdetlap1  34020  madjusmdetlem1  34021  madjusmdetlem2  34022  ccatmulgnn0dir  34736  plymulx  34742  itgexpif  34800  repr0  34805  elmrsubrn  35761  matunitlindflem1  37996  sticksstones12  42656  redvmptabs  42850  readvrec  42852  frlmvscadiccat  43009  fsuppind  43053  fsuppssindlem1  43054  reabsifneg  44089  reabsifnpos  44090  reabsifpos  44091  reabsifnneg  44092  reabssgn  44093  sqrtcval  44098  mnringmulrcld  44685  fourierdlem101  46662  hoidmv1lelem2  47047  dfafv2  47607  m1modmmod  47839  indprm  48119  indprmfz  48120  linc0scn0  48926  digexp  49110