Theorem ifeqda 4460

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 4431	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 485	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifeqda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
4	2, 3	eqtrd 2833	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
5		iffalse 4434	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 485	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifeqda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶)
8	6, 7	eqtrd 2833	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
9	4, 8	pm2.61dan 812	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1538  ifcif 4425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-if 4426

This theorem is referenced by:  somincom  5961  cantnfp1  9128  ccatsymb  13927  swrdccat3blem  14092  repswccat  14139  ccatco  14188  bitsinvp1  15788  xrsdsreval  20136  fvmptnn04if  21454  chfacfscmulgsum  21465  chfacfpmmulgsum  21469  oprpiece1res2  23557  phtpycc  23596  atantayl2  25524  ifeq3da  30313  fprodex01  30567  psgnfzto1stlem  30792  fzto1st1  30794  cycpm2tr  30811  mdetlap1  31179  madjusmdetlem1  31180  madjusmdetlem2  31181  ccatmulgnn0dir  31922  plymulx  31928  itgexpif  31987  repr0  31992  elmrsubrn  32880  matunitlindflem1  35053  frlmvscadiccat  39440  fsuppind  39456  fsuppssindlem1  39457  reabsifneg  40332  reabsifnpos  40333  reabsifpos  40334  reabsifnneg  40335  reabssgn  40336  sqrtcval  40341  mnringmulrcld  40936  fourierdlem101  42849  hoidmv1lelem2  43231  dfafv2  43688  linc0scn0  44832  m1modmmod  44935  digexp  45021