Theorem ifeqda 4564

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 4534	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 482	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifeqda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
4	2, 3	eqtrd 2772	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
5		iffalse 4537	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 482	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifeqda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶)
8	6, 7	eqtrd 2772	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
9	4, 8	pm2.61dan 811	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1541  ifcif 4528

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-if 4529

This theorem is referenced by:  somincom  6135  cantnfp1  9675  ccatsymb  14531  swrdccat3blem  14688  repswccat  14735  ccatco  14785  bitsinvp1  16389  xrsdsreval  20989  fvmptnn04if  22350  chfacfscmulgsum  22361  chfacfpmmulgsum  22365  oprpiece1res2  24467  phtpycc  24506  atantayl2  26440  ifeq3da  31773  fprodex01  32026  psgnfzto1stlem  32254  fzto1st1  32256  cycpm2tr  32273  elrspunsn  32542  mdetlap1  32801  madjusmdetlem1  32802  madjusmdetlem2  32803  ccatmulgnn0dir  33548  plymulx  33554  itgexpif  33613  repr0  33618  elmrsubrn  34506  matunitlindflem1  36479  sticksstones12  40969  frlmvscadiccat  41082  fsuppind  41164  fsuppssindlem1  41165  reabsifneg  42373  reabsifnpos  42374  reabsifpos  42375  reabsifnneg  42376  reabssgn  42377  sqrtcval  42382  mnringmulrcld  42977  fourierdlem101  44913  hoidmv1lelem2  45298  dfafv2  45830  linc0scn0  47094  m1modmmod  47197  digexp  47283