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

Theorem neeq2d 3003
 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 2781 . 2 (𝜑 → (𝐶 = 𝐴𝐶 = 𝐵))
32necon3bid 2987 1 (𝜑 → (𝐶𝐴𝐶𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   = wceq 1631   ≠ wne 2943 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751 This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764  df-ne 2944 This theorem is referenced by:  neeq2  3006  neeqtrd  3012  prneprprc  4526  fndifnfp  6586  f12dfv  6672  f13dfv  6673  infpssrlem4  9330  sqrt2irr  15185  dsmmval  20295  dsmmbas2  20298  frlmbas  20316  dfconn2  21443  alexsublem  22068  uc1pval  24119  mon1pval  24121  dchrsum2  25214  isinag  25950  uhgrwkspthlem2  26885  usgr2wlkneq  26887  usgr2trlspth  26892  lfgrn1cycl  26933  uspgrn2crct  26936  2pthdlem1  27077  3pthdlem1  27344  numclwwlk2lem1  27567  numclwwlk2lem1OLD  27574  eigorth  29037  eighmorth  29163  wlimeq12  32101  limsucncmpi  32781  poimirlem25  33767  poimirlem26  33768  pridlval  34164  maxidlval  34170  lshpset  34787  lduallkr3  34971  isatl  35108  cdlemk42  36750  stoweidlem43  40777  nnfoctbdjlem  41189
 Copyright terms: Public domain W3C validator