Theorem ifeqda 4528

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-if 4492

This theorem is referenced by:  somincom  6110  cantnfp1  9641  ccatsymb  14554  swrdccat3blem  14711  repswccat  14758  ccatco  14808  bitsinvp1  16426  xrsdsreval  21335  fvmptnn04if  22743  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  oprpiece1res2  24857  phtpycc  24897  atantayl2  26855  ifeq3da  32482  fprodex01  32757  psgnfzto1stlem  33064  fzto1st1  33066  cycpm2tr  33083  elrgspnlem4  33203  elrspunsn  33407  fldextrspunlsp  33676  mdetlap1  33823  madjusmdetlem1  33824  madjusmdetlem2  33825  ccatmulgnn0dir  34540  plymulx  34546  itgexpif  34604  repr0  34609  elmrsubrn  35514  matunitlindflem1  37617  sticksstones12  42153  redvmptabs  42355  readvrec  42357  frlmvscadiccat  42501  fsuppind  42585  fsuppssindlem1  42586  reabsifneg  43628  reabsifnpos  43629  reabsifpos  43630  reabsifnneg  43631  reabssgn  43632  sqrtcval  43637  mnringmulrcld  44224  fourierdlem101  46212  hoidmv1lelem2  46597  dfafv2  47137  m1modmmod  47363  linc0scn0  48416  digexp  48600