Theorem ifeqda 4522

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 4491	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 487	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifeqda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
4	2, 3	eqtrd 2798	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
5		iffalse 4494	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 487	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifeqda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶)
8	6, 7	eqtrd 2798	. 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 4485

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-if 4486

This theorem is used by:  somincom  6146  cantnfp1  9719  ccatsymb  14769  swrdccat3blem  14930  repswccat  14979  ccatco  15028  bitsinvp1  16663  xrsdsreval  21770  matunitlindflem1  23049  fvmptnn04if  23222  chfacfscmulgsum  23233  chfacfpmmulgsum  23237  oprpiece1res2  25328  phtpycc  25367  plymulidp  26658  atantayl2  27323  ifeq3da  33240  fprodex01  33512  psgnfzto1stlem  33760  fzto1st1  33762  cycpm2tr  33779  elrgspnlem4  33905  elrspunsn  34083  esplyfval1  34316  esplyind  34318  fldextrspunlsp  34417  mdetlap1  34569  madjusmdetlem1  34570  madjusmdetlem2  34571  ccatmulgnn0dir  35285  itgexpif  35346  repr0  35351  elmrsubrn  36493  sticksstones12  43474  redvmptabs  43677  readvrec  43679  frlmvscadiccat  43839  fsuppind  43884  fsuppssindlem1  43885  reabsifneg  44893  reabsifnpos  44894  reabsifpos  44895  reabsifnneg  44896  reabssgn  44897  sqrtcval  44902  mnringmulrcld  45487  fourierdlem101  47490  hoidmv1lelem2  47875  dfafv2  48475  m1modmmod  48707  indprm  48987  indprmfz  48988  linc0scn0  49866  digexp  50050