Theorem ifeqda 4567

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-if 4532

This theorem is referenced by:  somincom  6157  cantnfp1  9719  ccatsymb  14617  swrdccat3blem  14774  repswccat  14821  ccatco  14871  bitsinvp1  16483  xrsdsreval  21447  fvmptnn04if  22871  chfacfscmulgsum  22882  chfacfpmmulgsum  22886  oprpiece1res2  24997  phtpycc  25037  atantayl2  26996  ifeq3da  32567  fprodex01  32832  psgnfzto1stlem  33103  fzto1st1  33105  cycpm2tr  33122  elrgspnlem4  33235  elrspunsn  33437  mdetlap1  33787  madjusmdetlem1  33788  madjusmdetlem2  33789  ccatmulgnn0dir  34536  plymulx  34542  itgexpif  34600  repr0  34605  elmrsubrn  35505  matunitlindflem1  37603  sticksstones12  42140  redvmptabs  42369  readvrec  42371  frlmvscadiccat  42493  fsuppind  42577  fsuppssindlem1  42578  reabsifneg  43622  reabsifnpos  43623  reabsifpos  43624  reabsifnneg  43625  reabssgn  43626  sqrtcval  43631  mnringmulrcld  44224  fourierdlem101  46163  hoidmv1lelem2  46548  dfafv2  47082  linc0scn0  48269  m1modmmod  48371  digexp  48457