Theorem ifeqda 4524

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 4493	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 486	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifeqda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
4	2, 3	eqtrd 2798	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
5		iffalse 4496	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 486	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifeqda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶)
8	6, 7	eqtrd 2798	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
9	4, 8	pm2.61dan 824	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   = wceq 1570  ifcif 4487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-if 4488

This theorem is referenced by:  somincom  6134  cantnfp1  9646  ccatsymb  14616  swrdccat3blem  14772  repswccat  14819  ccatco  14868  bitsinvp1  16502  xrsdsreval  21562  fvmptnn04if  23006  chfacfscmulgsum  23017  chfacfpmmulgsum  23021  oprpiece1res2  25111  phtpycc  25150  plymulidp  26443  atantayl2  27103  ifeq3da  32892  fprodex01  33169  psgnfzto1stlem  33420  fzto1st1  33422  cycpm2tr  33439  elrgspnlem4  33565  elrspunsn  33737  esplyfval1  33963  esplyind  33965  fldextrspunlsp  34064  mdetlap1  34216  madjusmdetlem1  34217  madjusmdetlem2  34218  ccatmulgnn0dir  34932  itgexpif  34993  repr0  34998  elmrsubrn  36012  matunitlindflem1  38267  sticksstones12  42925  redvmptabs  43121  readvrec  43123  frlmvscadiccat  43280  fsuppind  43322  fsuppssindlem1  43323  reabsifneg  44358  reabsifnpos  44359  reabsifpos  44360  reabsifnneg  44361  reabssgn  44362  sqrtcval  44367  mnringmulrcld  44952  fourierdlem101  46921  hoidmv1lelem2  47306  dfafv2  47869  m1modmmod  48101  indprm  48381  indprmfz  48382  linc0scn0  49203  digexp  49387