Theorem ifeqda 4503

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1542  ifcif 4466

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-if 4467

This theorem is referenced by:  somincom  6097  cantnfp1  9602  ccatsymb  14545  swrdccat3blem  14701  repswccat  14748  ccatco  14797  bitsinvp1  16418  xrsdsreval  21392  fvmptnn04if  22814  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  oprpiece1res2  24919  phtpycc  24958  atantayl2  26902  ifeq3da  32616  fprodex01  32898  psgnfzto1stlem  33161  fzto1st1  33163  cycpm2tr  33180  elrgspnlem4  33306  elrspunsn  33489  esplyfval1  33717  esplyind  33719  fldextrspunlsp  33818  mdetlap1  33970  madjusmdetlem1  33971  madjusmdetlem2  33972  ccatmulgnn0dir  34686  plymulx  34692  itgexpif  34750  repr0  34755  elmrsubrn  35702  matunitlindflem1  37937  sticksstones12  42597  redvmptabs  42792  readvrec  42794  frlmvscadiccat  42951  fsuppind  43023  fsuppssindlem1  43024  reabsifneg  44059  reabsifnpos  44060  reabsifpos  44061  reabsifnneg  44062  reabssgn  44063  sqrtcval  44068  mnringmulrcld  44655  fourierdlem101  46635  hoidmv1lelem2  47020  dfafv2  47580  m1modmmod  47812  indprm  48092  indprmfz  48093  linc0scn0  48899  digexp  49083