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 2795	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
5		iffalse 4491	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 487	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifeqda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶)
8	6, 7	eqtrd 2795	. 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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4483

This theorem is used by:  somincom  6128  cantnfp1  9660  ccatsymb  14648  swrdccat3blem  14808  repswccat  14857  ccatco  14906  bitsinvp1  16539  xrsdsreval  21625  matunitlindflem1  22901  fvmptnn04if  23074  chfacfscmulgsum  23085  chfacfpmmulgsum  23089  oprpiece1res2  25180  phtpycc  25219  plymulidp  26512  atantayl2  27175  ifeq3da  33021  fprodex01  33295  psgnfzto1stlem  33540  fzto1st1  33542  cycpm2tr  33559  elrgspnlem4  33685  elrspunsn  33857  esplyfval1  34083  esplyind  34085  fldextrspunlsp  34184  mdetlap1  34336  madjusmdetlem1  34337  madjusmdetlem2  34338  ccatmulgnn0dir  35053  itgexpif  35114  repr0  35119  elmrsubrn  36099  sticksstones12  43024  redvmptabs  43235  readvrec  43237  frlmvscadiccat  43394  fsuppind  43436  fsuppssindlem1  43437  reabsifneg  44472  reabsifnpos  44473  reabsifpos  44474  reabsifnneg  44475  reabssgn  44476  sqrtcval  44481  mnringmulrcld  45066  fourierdlem101  47035  hoidmv1lelem2  47420  dfafv2  48020  m1modmmod  48252  indprm  48532  indprmfz  48533  linc0scn0  49353  digexp  49537