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

Theorem ifeqda 4486
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 4457 . . . 4 (𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐴)
21adantl 485 . . 3 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐴)
3 ifeqda.1 . . 3 ((𝜑𝜓) → 𝐴 = 𝐶)
42, 3eqtrd 2859 . 2 ((𝜑𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
5 iffalse 4460 . . . 4 𝜓 → if(𝜓, 𝐴, 𝐵) = 𝐵)
65adantl 485 . . 3 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐵)
7 ifeqda.2 . . 3 ((𝜑 ∧ ¬ 𝜓) → 𝐵 = 𝐶)
86, 7eqtrd 2859 . 2 ((𝜑 ∧ ¬ 𝜓) → if(𝜓, 𝐴, 𝐵) = 𝐶)
94, 8pm2.61dan 812 1 (𝜑 → if(𝜓, 𝐴, 𝐵) = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399   = wceq 1538  ifcif 4451
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-if 4452
This theorem is referenced by:  somincom  5982  cantnfp1  9142  ccatsymb  13939  swrdccat3blem  14104  repswccat  14151  ccatco  14200  bitsinvp1  15799  xrsdsreval  20593  fvmptnn04if  21460  chfacfscmulgsum  21471  chfacfpmmulgsum  21475  oprpiece1res2  23563  phtpycc  23602  atantayl2  25530  ifeq3da  30315  fprodex01  30555  psgnfzto1stlem  30777  fzto1st1  30779  cycpm2tr  30796  mdetlap1  31154  madjusmdetlem1  31155  madjusmdetlem2  31156  ccatmulgnn0dir  31872  plymulx  31878  itgexpif  31937  repr0  31942  elmrsubrn  32827  matunitlindflem1  34999  frlmvscadiccat  39374  reabsifneg  40249  reabsifnpos  40250  reabsifpos  40251  reabsifnneg  40252  reabssgn  40253  sqrtcval  40258  mnringmulrcld  40857  fourierdlem101  42776  hoidmv1lelem2  43158  dfafv2  43615  linc0scn0  44759  m1modmmod  44862  digexp  44948
  Copyright terms: Public domain W3C validator