Theorem ifeqda 4565

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   = wceq 1542  ifcif 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-if 4530

This theorem is referenced by:  somincom  6136  cantnfp1  9676  ccatsymb  14532  swrdccat3blem  14689  repswccat  14736  ccatco  14786  bitsinvp1  16390  xrsdsreval  20990  fvmptnn04if  22351  chfacfscmulgsum  22362  chfacfpmmulgsum  22366  oprpiece1res2  24468  phtpycc  24507  atantayl2  26443  ifeq3da  31809  fprodex01  32062  psgnfzto1stlem  32290  fzto1st1  32292  cycpm2tr  32309  elrspunsn  32578  mdetlap1  32837  madjusmdetlem1  32838  madjusmdetlem2  32839  ccatmulgnn0dir  33584  plymulx  33590  itgexpif  33649  repr0  33654  elmrsubrn  34542  matunitlindflem1  36532  sticksstones12  41022  frlmvscadiccat  41128  fsuppind  41210  fsuppssindlem1  41211  reabsifneg  42431  reabsifnpos  42432  reabsifpos  42433  reabsifnneg  42434  reabssgn  42435  sqrtcval  42440  mnringmulrcld  43035  fourierdlem101  44971  hoidmv1lelem2  45356  dfafv2  45888  linc0scn0  47152  m1modmmod  47255  digexp  47341