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

Theorem neeq2d 2837
Description: Deduction for inequality. (Contributed by NM, 25-Oct-1999.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
Hypothesis
Ref Expression
neeq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
neeq2d (𝜑 → (𝐶𝐴𝐶𝐵))

Proof of Theorem neeq2d
StepHypRef Expression
1 neeq1d.1 . . 3 (𝜑𝐴 = 𝐵)
21eqeq2d 2615 . 2 (𝜑 → (𝐶 = 𝐴𝐶 = 𝐵))
32necon3bid 2821 1 (𝜑 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wne 2775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-cleq 2598  df-ne 2777
This theorem is referenced by:  neeq2  2840  neeqtrd  2846  fndifnfp  6321  f12dfv  6403  f13dfv  6404  infpssrlem4  8984  sqrt2irr  14759  dsmmval  19835  dsmmbas2  19838  frlmbas  19856  dfcon2  20970  alexsublem  21596  uc1pval  23616  mon1pval  23618  dchrsum2  24706  isinag  25443  usgrcyclnl1  25930  numclwwlkovq  26388  eigorth  27883  eighmorth  28009  wlimeq12  30811  nofulllem5  30907  limsucncmpi  31416  poimirlem25  32403  poimirlem26  32404  pridlval  32801  maxidlval  32807  lshpset  33082  lduallkr3  33266  isatl  33403  cdlemk42  35046  stoweidlem43  38736  nnfoctbdjlem  39148  uhgr1wlkspthlem2  40958  usgr2wlkneq  40960  usgr2trlspth  40965  lfgrn1cycl  41006  uspgrn2crct  41009  2pthdlem1  41135  3pthdlem1  41329  av-numclwwlk2lem1  41530
  Copyright terms: Public domain W3C validator