Theorem ifeqda 4518

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-if 4482

This theorem is used by:  somincom  6129  cantnfp1  9687  ccatsymb  14733  swrdccat3blem  14894  repswccat  14943  ccatco  14992  bitsinvp1  16626  xrsdsreval  21725  matunitlindflem1  23001  fvmptnn04if  23174  chfacfscmulgsum  23185  chfacfpmmulgsum  23189  oprpiece1res2  25280  phtpycc  25319  plymulidp  26610  atantayl2  27273  ifeq3da  33191  fprodex01  33464  psgnfzto1stlem  33709  fzto1st1  33711  cycpm2tr  33728  elrgspnlem4  33854  elrspunsn  34027  esplyfval1  34253  esplyind  34255  fldextrspunlsp  34354  mdetlap1  34506  madjusmdetlem1  34507  madjusmdetlem2  34508  ccatmulgnn0dir  35222  itgexpif  35283  repr0  35288  elmrsubrn  36373  sticksstones12  43315  redvmptabs  43518  readvrec  43520  frlmvscadiccat  43680  fsuppind  43725  fsuppssindlem1  43726  reabsifneg  44739  reabsifnpos  44740  reabsifpos  44741  reabsifnneg  44742  reabssgn  44743  sqrtcval  44748  mnringmulrcld  45333  fourierdlem101  47324  hoidmv1lelem2  47709  dfafv2  48309  m1modmmod  48541  indprm  48821  indprmfz  48822  linc0scn0  49642  digexp  49826