Theorem necom 2726

Description: Commutation of inequality. (Contributed by NM, 14-May-1999.)

Assertion

Ref	Expression
necom

Proof of Theorem necom

Step	Hyp	Ref	Expression
1		eqcom 2466	. 2
2	1	necon3bii 2725	1

Syntax hints:  <->wb 184  =/=wne 2652

This theorem is referenced by:  necomi  2727  necomd  2728  0pss  3864  difprsn1  4166  difprsn2  4167  diftpsn3  4168  fndmdifcom  5992  fvpr1  6114  fvpr2  6115  fvpr1g  6116  fvtp1  6118  fvtp2  6119  fvtp3  6120  fvtp1g  6121  fvtp2g  6122  fvtp3g  6123  dff14b  6178  f12dfv  6179  f13dfv  6180  orduniorsuc  6665  kmlem3  8553  kmlem4  8554  ac6num  8880  leltne  9695  nn0lt2  10952  xrleltne  11380  fzofzim  11869  elfznelfzo  11915  elfznelfzob  11916  fleqceilz  11981  hashgt12el  12481  hashgt12el2  12482  cshw0  12765  cshwn  12768  cshwsdisj  14583  sgrp2nmndlem5  16047  f1omvdconj  16471  pmtrprfv3  16479  pmtr3ncomlem1  16498  dmdprdd  17030  xrsdsreclblem  18464  xrsdsreclb  18465  ordthaus  19885  hmphindis  20298  angpined  23161  nb3graprlem2  24452  nb3grapr  24453  cusgra3v  24464  usgrcyclnl2  24641  constr3lem6  24649  clwlkisclwwlklem2a4  24784  eupath2lem3  24979  frgra3v  25002  3vfriswmgra  25005  2pthfrgra  25011  3cyclfrgrarn1  25012  n4cyclfrgra  25018  frgranbnb  25020  frg2woteqm  25059  ch0pss  26363  cvmsdisj  28715  nosgnn0  29418  nodenselem4  29444  btwnouttr  29674  fscgr  29730  linecom  29800  linerflx2  29801  divrngidl  30425  prtlem90  30598  icccncfext  31690  fourierdlem42  31931  usgra2pthlem1  32353  usgra2pth0  32355  bnj563  33800  lcvbr3  34748  opltn0  34915  atlltn0  35031  2dim  35194  ps-2  35202  islln3  35234  llnexatN  35245  4atlem11  35333  isline4N  35501  lhpex2leN  35737  cdleme48gfv  36263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-cleq 2449  df-ne 2654