Theorem ifeqda 4521

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1540  ifcif 4484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-if 4485

This theorem is referenced by:  somincom  6095  cantnfp1  9610  ccatsymb  14523  swrdccat3blem  14680  repswccat  14727  ccatco  14777  bitsinvp1  16395  xrsdsreval  21304  fvmptnn04if  22712  chfacfscmulgsum  22723  chfacfpmmulgsum  22727  oprpiece1res2  24826  phtpycc  24866  atantayl2  26824  ifeq3da  32448  fprodex01  32723  psgnfzto1stlem  33030  fzto1st1  33032  cycpm2tr  33049  elrgspnlem4  33169  elrspunsn  33373  fldextrspunlsp  33642  mdetlap1  33789  madjusmdetlem1  33790  madjusmdetlem2  33791  ccatmulgnn0dir  34506  plymulx  34512  itgexpif  34570  repr0  34575  elmrsubrn  35480  matunitlindflem1  37583  sticksstones12  42119  redvmptabs  42321  readvrec  42323  frlmvscadiccat  42467  fsuppind  42551  fsuppssindlem1  42552  reabsifneg  43594  reabsifnpos  43595  reabsifpos  43596  reabsifnneg  43597  reabssgn  43598  sqrtcval  43603  mnringmulrcld  44190  fourierdlem101  46178  hoidmv1lelem2  46563  dfafv2  47106  m1modmmod  47332  linc0scn0  48385  digexp  48569