Theorem ifeqda 4495

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1539  ifcif 4459

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-if 4460

This theorem is referenced by:  somincom  6039  cantnfp1  9439  ccatsymb  14287  swrdccat3blem  14452  repswccat  14499  ccatco  14548  bitsinvp1  16156  xrsdsreval  20643  fvmptnn04if  21998  chfacfscmulgsum  22009  chfacfpmmulgsum  22013  oprpiece1res2  24115  phtpycc  24154  atantayl2  26088  ifeq3da  30889  fprodex01  31139  psgnfzto1stlem  31367  fzto1st1  31369  cycpm2tr  31386  mdetlap1  31776  madjusmdetlem1  31777  madjusmdetlem2  31778  ccatmulgnn0dir  32521  plymulx  32527  itgexpif  32586  repr0  32591  elmrsubrn  33482  matunitlindflem1  35773  sticksstones12  40114  frlmvscadiccat  40237  fsuppind  40279  fsuppssindlem1  40280  reabsifneg  41240  reabsifnpos  41241  reabsifpos  41242  reabsifnneg  41243  reabssgn  41244  sqrtcval  41249  mnringmulrcld  41846  fourierdlem101  43748  hoidmv1lelem2  44130  dfafv2  44624  linc0scn0  45764  m1modmmod  45867  digexp  45953