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

Theorem neeq2d 3001
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 2744 . 2 (𝜑 → (𝐶 = 𝐴𝐶 = 𝐵))
32necon3bid 2985 1 (𝜑 → (𝐶𝐴𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  wne 2940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2941
This theorem is referenced by:  neeq2  3004  neeqtrd  3010  prneprprc  4819  fndifnfp  7123  f12dfv  7220  f13dfv  7221  infpssrlem4  10247  sqrt2irr  16136  dsmmval  21156  dsmmbas2  21159  frlmbas  21177  dfconn2  22786  alexsublem  23411  uc1pval  25520  mon1pval  25522  dchrsum2  26632  noetainflem4  27104  isinag  27822  uhgrwkspthlem2  28744  usgr2wlkneq  28746  usgr2trlspth  28751  lfgrn1cycl  28792  uspgrn2crct  28795  2pthdlem1  28917  3pthdlem1  29150  numclwwlk2lem1  29362  eigorth  30822  eighmorth  30948  prmidlval  32257  mxidlval  32278  ressply1mon1p  32327  wlimeq12  34450  limsucncmpi  34963  poimirlem25  36149  poimirlem26  36150  pridlval  36538  maxidlval  36544  lshpset  37486  lduallkr3  37670  isatl  37807  cdlemk42  39450  sdrgunit  40760  prjspner1  41007  dffltz  41015  stoweidlem43  44370  nnfoctbdjlem  44782
  Copyright terms: Public domain W3C validator