Theorem ifeqda 4537

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-if 4501

This theorem is referenced by:  somincom  6123  cantnfp1  9695  ccatsymb  14600  swrdccat3blem  14757  repswccat  14804  ccatco  14854  bitsinvp1  16468  xrsdsreval  21379  fvmptnn04if  22787  chfacfscmulgsum  22798  chfacfpmmulgsum  22802  oprpiece1res2  24901  phtpycc  24941  atantayl2  26900  ifeq3da  32527  fprodex01  32804  psgnfzto1stlem  33111  fzto1st1  33113  cycpm2tr  33130  elrgspnlem4  33240  elrspunsn  33444  fldextrspunlsp  33715  mdetlap1  33857  madjusmdetlem1  33858  madjusmdetlem2  33859  ccatmulgnn0dir  34574  plymulx  34580  itgexpif  34638  repr0  34643  elmrsubrn  35542  matunitlindflem1  37640  sticksstones12  42171  redvmptabs  42403  readvrec  42405  frlmvscadiccat  42529  fsuppind  42613  fsuppssindlem1  42614  reabsifneg  43656  reabsifnpos  43657  reabsifpos  43658  reabsifnneg  43659  reabssgn  43660  sqrtcval  43665  mnringmulrcld  44252  fourierdlem101  46236  hoidmv1lelem2  46621  dfafv2  47161  linc0scn0  48399  m1modmmod  48501  digexp  48587