MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  necon3bbii Unicode version

Theorem necon3bbii 2718
Description: Deduction from equality to inequality. (Contributed by NM, 13-Apr-2007.)
Hypothesis
Ref Expression
necon3bbii.1
Assertion
Ref Expression
necon3bbii

Proof of Theorem necon3bbii
StepHypRef Expression
1 necon3bbii.1 . . . 4
21bicomi 202 . . 3
32necon3abii 2717 . 2
43bicomi 202 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  <->wb 184  =wceq 1395  =/=wne 2652
This theorem is referenced by:  necon1abii  2719  nssinpss  3729  difsnpss  4173  ordintdif  4932  xpdifid  5440  tfi  6688  oelim2  7263  0sdomg  7666  fin23lem26  8726  axdc3lem4  8854  axdc4lem  8856  axcclem  8858  crreczi  12291  ef0lem  13814  lidlnz  17876  nconsubb  19924  ufileu  20420  itg2cnlem1  22168  plyeq0lem  22607  abelthlem2  22827  ppinprm  23426  chtnprm  23428  ltgov  23983  shne0i  26366  pjneli  26641  eleigvec  26876  nmo  27384  qqhval2lem  27962  qqhval2  27963  sibfof  28282  dffr5  29182  wfi  29287  frind  29323  ellimits  29560  itg2addnclem2  30067  ftc1anclem3  30092  elicc3  30135  limcrecl  31635  usgra2pthlem1  32353  onfrALTlem5  33314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-ne 2654
  Copyright terms: Public domain W3C validator