Theorem ifeqda 4504

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   = wceq 1537  ifcif 4469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-if 4470

This theorem is referenced by:  somincom  5996  cantnfp1  9146  ccatsymb  13938  swrdccat3blem  14103  repswccat  14150  ccatco  14199  bitsinvp1  15800  xrsdsreval  20592  fvmptnn04if  21459  chfacfscmulgsum  21470  chfacfpmmulgsum  21474  oprpiece1res2  23558  phtpycc  23597  atantayl2  25518  ifeq3da  30303  fprodex01  30543  psgnfzto1stlem  30744  fzto1st1  30746  cycpm2tr  30763  mdetlap1  31093  madjusmdetlem1  31094  madjusmdetlem2  31095  ccatmulgnn0dir  31814  plymulx  31820  itgexpif  31879  repr0  31884  elmrsubrn  32769  matunitlindflem1  34890  frlmvscadiccat  39152  fourierdlem101  42499  hoidmv1lelem2  42881  dfafv2  43338  linc0scn0  44485  m1modmmod  44588  digexp  44674