Theorem ifeqda 4513

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1541  ifcif 4476

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-if 4477

This theorem is referenced by:  somincom  6088  cantnfp1  9582  ccatsymb  14497  swrdccat3blem  14653  repswccat  14700  ccatco  14749  bitsinvp1  16367  xrsdsreval  21357  fvmptnn04if  22784  chfacfscmulgsum  22795  chfacfpmmulgsum  22799  oprpiece1res2  24897  phtpycc  24937  atantayl2  26895  ifeq3da  32547  fprodex01  32834  psgnfzto1stlem  33110  fzto1st1  33112  cycpm2tr  33129  elrgspnlem4  33255  elrspunsn  33438  esplyind  33659  fldextrspunlsp  33759  mdetlap1  33911  madjusmdetlem1  33912  madjusmdetlem2  33913  ccatmulgnn0dir  34627  plymulx  34633  itgexpif  34691  repr0  34696  elmrsubrn  35636  matunitlindflem1  37729  sticksstones12  42324  redvmptabs  42530  readvrec  42532  frlmvscadiccat  42676  fsuppind  42748  fsuppssindlem1  42749  reabsifneg  43789  reabsifnpos  43790  reabsifpos  43791  reabsifnneg  43792  reabssgn  43793  sqrtcval  43798  mnringmulrcld  44385  fourierdlem101  46367  hoidmv1lelem2  46752  dfafv2  47294  m1modmmod  47520  linc0scn0  48585  digexp  48769