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

Theorem neeq2d 2842
 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 2620 . 2 (𝜑 → (𝐶 = 𝐴𝐶 = 𝐵))
32necon3bid 2826 1 (𝜑 → (𝐶𝐴𝐶𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   ≠ wne 2780 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782 This theorem is referenced by:  neeq2  2845  neeqtrd  2851  fndifnfp  6347  f12dfv  6429  f13dfv  6430  infpssrlem4  9011  sqrt2irr  14817  dsmmval  19897  dsmmbas2  19900  frlmbas  19918  dfcon2  21032  alexsublem  21658  uc1pval  23703  mon1pval  23705  dchrsum2  24793  isinag  25529  usgrcyclnl1  26168  numclwwlkovq  26626  eigorth  28081  eighmorth  28207  wlimeq12  31009  nofulllem5  31105  limsucncmpi  31614  poimirlem25  32604  poimirlem26  32605  pridlval  33002  maxidlval  33008  lshpset  33283  lduallkr3  33467  isatl  33604  cdlemk42  35247  stoweidlem43  38936  nnfoctbdjlem  39348  uhgr1wlkspthlem2  40960  usgr2wlkneq  40962  usgr2trlspth  40967  lfgrn1cycl  41008  uspgrn2crct  41011  2pthdlem1  41137  3pthdlem1  41331  av-numclwwlk2lem1  41532
 Copyright terms: Public domain W3C validator