Theorem ifeqda 4584

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1537  ifcif 4548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-if 4549

This theorem is referenced by:  somincom  6166  cantnfp1  9750  ccatsymb  14630  swrdccat3blem  14787  repswccat  14834  ccatco  14884  bitsinvp1  16495  xrsdsreval  21452  fvmptnn04if  22876  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  oprpiece1res2  25002  phtpycc  25042  atantayl2  26999  ifeq3da  32569  fprodex01  32829  psgnfzto1stlem  33093  fzto1st1  33095  cycpm2tr  33112  elrspunsn  33422  mdetlap1  33772  madjusmdetlem1  33773  madjusmdetlem2  33774  ccatmulgnn0dir  34519  plymulx  34525  itgexpif  34583  repr0  34588  elmrsubrn  35488  matunitlindflem1  37576  sticksstones12  42115  frlmvscadiccat  42461  fsuppind  42545  fsuppssindlem1  42546  reabsifneg  43594  reabsifnpos  43595  reabsifpos  43596  reabsifnneg  43597  reabssgn  43598  sqrtcval  43603  mnringmulrcld  44197  fourierdlem101  46128  hoidmv1lelem2  46513  dfafv2  47047  linc0scn0  48152  m1modmmod  48255  digexp  48341