Theorem ifeqda 4515

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540  ifcif 4478

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4479

This theorem is referenced by:  somincom  6087  cantnfp1  9596  ccatsymb  14508  swrdccat3blem  14664  repswccat  14711  ccatco  14761  bitsinvp1  16379  xrsdsreval  21337  fvmptnn04if  22753  chfacfscmulgsum  22764  chfacfpmmulgsum  22768  oprpiece1res2  24867  phtpycc  24907  atantayl2  26865  ifeq3da  32509  fprodex01  32789  psgnfzto1stlem  33061  fzto1st1  33063  cycpm2tr  33080  elrgspnlem4  33204  elrspunsn  33385  fldextrspunlsp  33660  mdetlap1  33812  madjusmdetlem1  33813  madjusmdetlem2  33814  ccatmulgnn0dir  34529  plymulx  34535  itgexpif  34593  repr0  34598  elmrsubrn  35512  matunitlindflem1  37615  sticksstones12  42151  redvmptabs  42353  readvrec  42355  frlmvscadiccat  42499  fsuppind  42583  fsuppssindlem1  42584  reabsifneg  43625  reabsifnpos  43626  reabsifpos  43627  reabsifnneg  43628  reabssgn  43629  sqrtcval  43634  mnringmulrcld  44221  fourierdlem101  46208  hoidmv1lelem2  46593  dfafv2  47136  m1modmmod  47362  linc0scn0  48428  digexp  48612