Theorem ifeqda 4525

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4489

This theorem is referenced by:  somincom  6107  cantnfp1  9634  ccatsymb  14547  swrdccat3blem  14704  repswccat  14751  ccatco  14801  bitsinvp1  16419  xrsdsreval  21328  fvmptnn04if  22736  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  oprpiece1res2  24850  phtpycc  24890  atantayl2  26848  ifeq3da  32475  fprodex01  32750  psgnfzto1stlem  33057  fzto1st1  33059  cycpm2tr  33076  elrgspnlem4  33196  elrspunsn  33400  fldextrspunlsp  33669  mdetlap1  33816  madjusmdetlem1  33817  madjusmdetlem2  33818  ccatmulgnn0dir  34533  plymulx  34539  itgexpif  34597  repr0  34602  elmrsubrn  35507  matunitlindflem1  37610  sticksstones12  42146  redvmptabs  42348  readvrec  42350  frlmvscadiccat  42494  fsuppind  42578  fsuppssindlem1  42579  reabsifneg  43621  reabsifnpos  43622  reabsifpos  43623  reabsifnneg  43624  reabssgn  43625  sqrtcval  43630  mnringmulrcld  44217  fourierdlem101  46205  hoidmv1lelem2  46590  dfafv2  47133  m1modmmod  47359  linc0scn0  48412  digexp  48596