Theorem ifeqda 4516

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1541  ifcif 4479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4480

This theorem is referenced by:  somincom  6091  cantnfp1  9590  ccatsymb  14506  swrdccat3blem  14662  repswccat  14709  ccatco  14758  bitsinvp1  16376  xrsdsreval  21366  fvmptnn04if  22793  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  oprpiece1res2  24906  phtpycc  24946  atantayl2  26904  ifeq3da  32621  fprodex01  32906  psgnfzto1stlem  33182  fzto1st1  33184  cycpm2tr  33201  elrgspnlem4  33327  elrspunsn  33510  esplyind  33731  fldextrspunlsp  33831  mdetlap1  33983  madjusmdetlem1  33984  madjusmdetlem2  33985  ccatmulgnn0dir  34699  plymulx  34705  itgexpif  34763  repr0  34768  elmrsubrn  35714  matunitlindflem1  37817  sticksstones12  42412  redvmptabs  42615  readvrec  42617  frlmvscadiccat  42761  fsuppind  42833  fsuppssindlem1  42834  reabsifneg  43873  reabsifnpos  43874  reabsifpos  43875  reabsifnneg  43876  reabssgn  43877  sqrtcval  43882  mnringmulrcld  44469  fourierdlem101  46451  hoidmv1lelem2  46836  dfafv2  47378  m1modmmod  47604  linc0scn0  48669  digexp  48853