Theorem ifeqda 4566

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 4536	. . . 4 ⊢ (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
2	1	adantl 480	. . 3 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3		ifeqda.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝐴 = 𝐶)
4	2, 3	eqtrd 2765	. 2 ⊢ ((𝜑 ∧ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
5		iffalse 4539	. . . 4 ⊢ (¬ 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
6	5	adantl 480	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7		ifeqda.2	. . 3 ⊢ ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶)
8	6, 7	eqtrd 2765	. 2 ⊢ ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
9	4, 8	pm2.61dan 811	1 ⊢ (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394   = wceq 1533  ifcif 4530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-if 4531

This theorem is referenced by:  somincom  6141  cantnfp1  9706  ccatsymb  14568  swrdccat3blem  14725  repswccat  14772  ccatco  14822  bitsinvp1  16427  xrsdsreval  21361  fvmptnn04if  22795  chfacfscmulgsum  22806  chfacfpmmulgsum  22810  oprpiece1res2  24921  phtpycc  24961  atantayl2  26915  ifeq3da  32416  fprodex01  32673  psgnfzto1stlem  32913  fzto1st1  32915  cycpm2tr  32932  elrspunsn  33241  mdetlap1  33555  madjusmdetlem1  33556  madjusmdetlem2  33557  ccatmulgnn0dir  34302  plymulx  34308  itgexpif  34366  repr0  34371  elmrsubrn  35258  matunitlindflem1  37217  sticksstones12  41758  frlmvscadiccat  41881  fsuppind  41955  fsuppssindlem1  41956  reabsifneg  43201  reabsifnpos  43202  reabsifpos  43203  reabsifnneg  43204  reabssgn  43205  sqrtcval  43210  mnringmulrcld  43804  fourierdlem101  45730  hoidmv1lelem2  46115  dfafv2  46647  linc0scn0  47674  m1modmmod  47777  digexp  47863