Theorem ifeqda 4562

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-if 4526

This theorem is referenced by:  somincom  6154  cantnfp1  9721  ccatsymb  14620  swrdccat3blem  14777  repswccat  14824  ccatco  14874  bitsinvp1  16486  xrsdsreval  21429  fvmptnn04if  22855  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  oprpiece1res2  24983  phtpycc  25023  atantayl2  26981  ifeq3da  32559  fprodex01  32827  psgnfzto1stlem  33120  fzto1st1  33122  cycpm2tr  33139  elrgspnlem4  33249  elrspunsn  33457  fldextrspunlsp  33724  mdetlap1  33825  madjusmdetlem1  33826  madjusmdetlem2  33827  ccatmulgnn0dir  34557  plymulx  34563  itgexpif  34621  repr0  34626  elmrsubrn  35525  matunitlindflem1  37623  sticksstones12  42159  redvmptabs  42390  readvrec  42392  frlmvscadiccat  42516  fsuppind  42600  fsuppssindlem1  42601  reabsifneg  43645  reabsifnpos  43646  reabsifpos  43647  reabsifnneg  43648  reabssgn  43649  sqrtcval  43654  mnringmulrcld  44247  fourierdlem101  46222  hoidmv1lelem2  46607  dfafv2  47144  linc0scn0  48340  m1modmmod  48442  digexp  48528