Theorem ifeqda 4518

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1542  ifcif 4481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4482

This theorem is referenced by:  somincom  6099  cantnfp1  9602  ccatsymb  14518  swrdccat3blem  14674  repswccat  14721  ccatco  14770  bitsinvp1  16388  xrsdsreval  21378  fvmptnn04if  22805  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  oprpiece1res2  24918  phtpycc  24958  atantayl2  26916  ifeq3da  32633  fprodex01  32917  psgnfzto1stlem  33194  fzto1st1  33196  cycpm2tr  33213  elrgspnlem4  33339  elrspunsn  33522  esplyfval1  33750  esplyind  33752  fldextrspunlsp  33852  mdetlap1  34004  madjusmdetlem1  34005  madjusmdetlem2  34006  ccatmulgnn0dir  34720  plymulx  34726  itgexpif  34784  repr0  34789  elmrsubrn  35736  matunitlindflem1  37867  sticksstones12  42528  redvmptabs  42730  readvrec  42732  frlmvscadiccat  42876  fsuppind  42948  fsuppssindlem1  42949  reabsifneg  43988  reabsifnpos  43989  reabsifpos  43990  reabsifnneg  43991  reabssgn  43992  sqrtcval  43997  mnringmulrcld  44584  fourierdlem101  46565  hoidmv1lelem2  46950  dfafv2  47492  m1modmmod  47718  linc0scn0  48783  digexp  48967