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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-if 4468

This theorem is referenced by:  somincom  6091  cantnfp1  9593  ccatsymb  14536  swrdccat3blem  14692  repswccat  14739  ccatco  14788  bitsinvp1  16409  xrsdsreval  21401  fvmptnn04if  22824  chfacfscmulgsum  22835  chfacfpmmulgsum  22839  oprpiece1res2  24929  phtpycc  24968  atantayl2  26915  ifeq3da  32631  fprodex01  32913  psgnfzto1stlem  33176  fzto1st1  33178  cycpm2tr  33195  elrgspnlem4  33321  elrspunsn  33504  esplyfval1  33732  esplyind  33734  fldextrspunlsp  33834  mdetlap1  33986  madjusmdetlem1  33987  madjusmdetlem2  33988  ccatmulgnn0dir  34702  plymulx  34708  itgexpif  34766  repr0  34771  elmrsubrn  35718  matunitlindflem1  37951  sticksstones12  42611  redvmptabs  42806  readvrec  42808  frlmvscadiccat  42965  fsuppind  43037  fsuppssindlem1  43038  reabsifneg  44077  reabsifnpos  44078  reabsifpos  44079  reabsifnneg  44080  reabssgn  44081  sqrtcval  44086  mnringmulrcld  44673  fourierdlem101  46653  hoidmv1lelem2  47038  dfafv2  47592  m1modmmod  47824  indprm  48104  indprmfz  48105  linc0scn0  48911  digexp  49095