Theorem ifeqda 4526

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 4495	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 487	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifeqda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
4	2, 3	eqtrd 2800	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
5		iffalse 4498	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 487	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifeqda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶)
8	6, 7	eqtrd 2800	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
9	4, 8	pm2.61dan 825	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1570  ifcif 4489

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-if 4490

This theorem is used by:  somincom  6136  cantnfp1  9653  ccatsymb  14634  swrdccat3blem  14794  repswccat  14843  ccatco  14892  bitsinvp1  16525  xrsdsreval  21592  fvmptnn04if  23036  chfacfscmulgsum  23047  chfacfpmmulgsum  23051  oprpiece1res2  25142  phtpycc  25181  plymulidp  26474  atantayl2  27134  ifeq3da  32939  fprodex01  33215  psgnfzto1stlem  33460  fzto1st1  33462  cycpm2tr  33479  elrgspnlem4  33605  elrspunsn  33777  esplyfval1  34003  esplyind  34005  fldextrspunlsp  34104  mdetlap1  34256  madjusmdetlem1  34257  madjusmdetlem2  34258  ccatmulgnn0dir  34973  itgexpif  35034  repr0  35039  elmrsubrn  36025  matunitlindflem1  38300  sticksstones12  42958  redvmptabs  43154  readvrec  43156  frlmvscadiccat  43313  fsuppind  43355  fsuppssindlem1  43356  reabsifneg  44391  reabsifnpos  44392  reabsifpos  44393  reabsifnneg  44394  reabssgn  44395  sqrtcval  44400  mnringmulrcld  44985  fourierdlem101  46954  hoidmv1lelem2  47339  dfafv2  47902  m1modmmod  48134  indprm  48414  indprmfz  48415  linc0scn0  49236  digexp  49420