Theorem ifeqda 4492

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1539  ifcif 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-if 4457

This theorem is referenced by:  somincom  6028  cantnfp1  9369  ccatsymb  14215  swrdccat3blem  14380  repswccat  14427  ccatco  14476  bitsinvp1  16084  xrsdsreval  20555  fvmptnn04if  21906  chfacfscmulgsum  21917  chfacfpmmulgsum  21921  oprpiece1res2  24021  phtpycc  24060  atantayl2  25993  ifeq3da  30790  fprodex01  31041  psgnfzto1stlem  31269  fzto1st1  31271  cycpm2tr  31288  mdetlap1  31678  madjusmdetlem1  31679  madjusmdetlem2  31680  ccatmulgnn0dir  32421  plymulx  32427  itgexpif  32486  repr0  32491  elmrsubrn  33382  matunitlindflem1  35700  sticksstones12  40042  frlmvscadiccat  40163  fsuppind  40202  fsuppssindlem1  40203  reabsifneg  41129  reabsifnpos  41130  reabsifpos  41131  reabsifnneg  41132  reabssgn  41133  sqrtcval  41138  mnringmulrcld  41735  fourierdlem101  43638  hoidmv1lelem2  44020  dfafv2  44511  linc0scn0  45652  m1modmmod  45755  digexp  45841