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

Theorem ifeqda 4526
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 4496 . . . 4 (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
21adantl 483 . . 3 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3 ifeqda.1 . . 3 ((𝜑𝜓) → 𝐴 = 𝐶)
42, 3eqtrd 2773 . 2 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
5 iffalse 4499 . . . 4 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
65adantl 483 . . 3 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7 ifeqda.2 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶)
86, 7eqtrd 2773 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
94, 8pm2.61dan 812 1 (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397   = wceq 1542  ifcif 4490
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 4491
This theorem is referenced by:  somincom  6092  cantnfp1  9625  ccatsymb  14479  swrdccat3blem  14636  repswccat  14683  ccatco  14733  bitsinvp1  16337  xrsdsreval  20865  fvmptnn04if  22221  chfacfscmulgsum  22232  chfacfpmmulgsum  22236  oprpiece1res2  24338  phtpycc  24377  atantayl2  26311  ifeq3da  31518  fprodex01  31777  psgnfzto1stlem  32005  fzto1st1  32007  cycpm2tr  32024  mdetlap1  32471  madjusmdetlem1  32472  madjusmdetlem2  32473  ccatmulgnn0dir  33218  plymulx  33224  itgexpif  33283  repr0  33288  elmrsubrn  34178  matunitlindflem1  36124  sticksstones12  40616  frlmvscadiccat  40730  fsuppind  40812  fsuppssindlem1  40813  reabsifneg  41996  reabsifnpos  41997  reabsifpos  41998  reabsifnneg  41999  reabssgn  42000  sqrtcval  42005  mnringmulrcld  42600  fourierdlem101  44538  hoidmv1lelem2  44923  dfafv2  45454  linc0scn0  46594  m1modmmod  46697  digexp  46783
  Copyright terms: Public domain W3C validator