MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ifeqda Structured version   Visualization version   GIF version

Theorem ifeqda 4566
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
StepHypRef Expression
1 iftrue 4536 . . . 4 (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
21adantl 480 . . 3 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3 ifeqda.1 . . 3 ((𝜑𝜓) → 𝐴 = 𝐶)
42, 3eqtrd 2765 . 2 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
5 iffalse 4539 . . . 4 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
65adantl 480 . . 3 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7 ifeqda.2 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶)
86, 7eqtrd 2765 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
94, 8pm2.61dan 811 1 (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394   = wceq 1533  ifcif 4530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-if 4531
This theorem is referenced by:  somincom  6141  cantnfp1  9706  ccatsymb  14568  swrdccat3blem  14725  repswccat  14772  ccatco  14822  bitsinvp1  16427  xrsdsreval  21361  fvmptnn04if  22795  chfacfscmulgsum  22806  chfacfpmmulgsum  22810  oprpiece1res2  24921  phtpycc  24961  atantayl2  26915  ifeq3da  32416  fprodex01  32673  psgnfzto1stlem  32913  fzto1st1  32915  cycpm2tr  32932  elrspunsn  33241  mdetlap1  33555  madjusmdetlem1  33556  madjusmdetlem2  33557  ccatmulgnn0dir  34302  plymulx  34308  itgexpif  34366  repr0  34371  elmrsubrn  35258  matunitlindflem1  37217  sticksstones12  41758  frlmvscadiccat  41881  fsuppind  41955  fsuppssindlem1  41956  reabsifneg  43201  reabsifnpos  43202  reabsifpos  43203  reabsifnneg  43204  reabssgn  43205  sqrtcval  43210  mnringmulrcld  43804  fourierdlem101  45730  hoidmv1lelem2  46115  dfafv2  46647  linc0scn0  47674  m1modmmod  47777  digexp  47863
  Copyright terms: Public domain W3C validator