Theorem ifeqda 4519

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 4488	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 487	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifeqda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
4	2, 3	eqtrd 2796	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
5		iffalse 4491	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 487	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifeqda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶)
8	6, 7	eqtrd 2796	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
9	4, 8	pm2.61dan 825	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1570  ifcif 4482

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-if 4483

This theorem is used by:  somincom  6128  cantnfp1  9675  ccatsymb  14721  swrdccat3blem  14881  repswccat  14930  ccatco  14979  bitsinvp1  16612  xrsdsreval  21711  matunitlindflem1  22987  fvmptnn04if  23160  chfacfscmulgsum  23171  chfacfpmmulgsum  23175  oprpiece1res2  25266  phtpycc  25305  plymulidp  26596  atantayl2  27259  ifeq3da  33135  fprodex01  33409  psgnfzto1stlem  33654  fzto1st1  33656  cycpm2tr  33673  elrgspnlem4  33799  elrspunsn  33972  esplyfval1  34198  esplyind  34200  fldextrspunlsp  34299  mdetlap1  34451  madjusmdetlem1  34452  madjusmdetlem2  34453  ccatmulgnn0dir  35167  itgexpif  35228  repr0  35233  elmrsubrn  36264  sticksstones12  43188  redvmptabs  43391  readvrec  43393  frlmvscadiccat  43553  fsuppind  43598  fsuppssindlem1  43599  reabsifneg  44617  reabsifnpos  44618  reabsifpos  44619  reabsifnneg  44620  reabssgn  44621  sqrtcval  44626  mnringmulrcld  45211  fourierdlem101  47186  hoidmv1lelem2  47571  dfafv2  48171  m1modmmod  48403  indprm  48683  indprmfz  48684  linc0scn0  49504  digexp  49688