Theorem ifeqda 4491

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 4460	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 482	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifeqda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
4	2, 3	eqtrd 2774	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
5		iffalse 4463	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 482	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifeqda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶)
8	6, 7	eqtrd 2774	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
9	4, 8	pm2.61dan 818	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1547  ifcif 4454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-if 4455

This theorem is referenced by:  somincom  6084  cantnfp1  9593  ccatsymb  14536  swrdccat3blem  14692  repswccat  14739  ccatco  14788  bitsinvp1  16409  xrsdsreval  21387  fvmptnn04if  22832  chfacfscmulgsum  22843  chfacfpmmulgsum  22847  oprpiece1res2  24937  phtpycc  24976  atantayl2  26920  ifeq3da  32634  fprodex01  32917  psgnfzto1stlem  33181  fzto1st1  33183  cycpm2tr  33200  elrgspnlem4  33326  elrspunsn  33512  esplyfval1  33757  esplyind  33759  fldextrspunlsp  33858  mdetlap1  34010  madjusmdetlem1  34011  madjusmdetlem2  34012  ccatmulgnn0dir  34726  plymulx  34732  itgexpif  34790  repr0  34795  elmrsubrn  35748  matunitlindflem1  37983  sticksstones12  42643  redvmptabs  42837  readvrec  42839  frlmvscadiccat  42996  fsuppind  43040  fsuppssindlem1  43041  reabsifneg  44076  reabsifnpos  44077  reabsifpos  44078  reabsifnneg  44079  reabssgn  44080  sqrtcval  44085  mnringmulrcld  44672  fourierdlem101  46650  hoidmv1lelem2  47035  dfafv2  47595  m1modmmod  47827  indprm  48107  indprmfz  48108  linc0scn0  48914  digexp  49098