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

Theorem neeq2d 3076
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 2832 . 2 (𝜑 → (𝐶 = 𝐴𝐶 = 𝐵))
32necon3bid 3060 1 (𝜑 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wne 3016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-ne 3017
This theorem is referenced by:  neeq2  3079  neeqtrd  3085  prneprprc  4785  fndifnfp  6931  f12dfv  7021  f13dfv  7022  infpssrlem4  9717  sqrt2irr  15592  dsmmval  20808  dsmmbas2  20811  frlmbas  20829  dfconn2  21957  alexsublem  22582  uc1pval  24662  mon1pval  24664  dchrsum2  25772  isinag  26552  uhgrwkspthlem2  27463  usgr2wlkneq  27465  usgr2trlspth  27470  lfgrn1cycl  27511  uspgrn2crct  27514  2pthdlem1  27637  3pthdlem1  27871  numclwwlk2lem1  28083  eigorth  29543  eighmorth  29669  prmidlval  30874  wlimeq12  33004  limsucncmpi  33691  poimirlem25  34799  poimirlem26  34800  pridlval  35194  maxidlval  35200  lshpset  35996  lduallkr3  36180  isatl  36317  cdlemk42  37959  dffltz  39151  stoweidlem43  42209  nnfoctbdjlem  42618
  Copyright terms: Public domain W3C validator