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

Theorem necom 2687
Description: Commutation of inequality. (Contributed by NM, 14-May-1999.)
Assertion
Ref Expression
necom  |-  ( A  =/=  B  <->  B  =/=  A )

Proof of Theorem necom
StepHypRef Expression
1 eqcom 2440 . 2  |-  ( A  =  B  <->  B  =  A )
21necon3bii 2635 1  |-  ( A  =/=  B  <->  B  =/=  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    =/= wne 2601
This theorem is referenced by:  necomi  2688  necomd  2689  0pss  3667  difprsn1  3937  difprsn2  3938  diftpsn3  3939  orduniorsuc  4813  fndmdifcom  5838  fvpr1  5938  fvpr2  5939  fvpr1g  5940  fvtp1  5942  fvtp2  5943  fvtp3  5944  fvtp1g  5945  fvtp2g  5946  fvtp3g  5947  kmlem3  8037  kmlem4  8038  ac6num  8364  leltne  9169  xrleltne  10743  elfznelfzo  11197  elfznelfzob  11198  hashgt12el  11687  hashgt12el2  11688  dmdprdd  15565  xrsdsreclblem  16749  xrsdsreclb  16750  ordthaus  17453  hmphindis  17834  angpined  20676  nb3graprlem2  21466  nb3grapr  21467  cusgra3v  21478  usgrcyclnl2  21633  constr3lem6  21641  eupath2lem3  21706  ch0pss  22952  iundisj2f  24035  iundisj2fi  24158  cvmsdisj  24962  cvmscld  24965  nosgnn0  25618  nodenselem4  25644  btwnouttr  25963  fscgr  26019  linecom  26089  linerflx2  26090  divrngidl  26652  prtlem90  26720  cmpfiiin  26765  uvcvv0  27230  f1omvdconj  27380  dff14b  28097  f12dfv  28098  f13dfv  28099  fzofzim  28159  cshwssizelem2  28315  cshwsdisj  28319  usgra2pthlem1  28348  usgra2pth0  28350  frgra3v  28466  3vfriswmgra  28469  2pthfrgra  28475  3cyclfrgrarn1  28476  n4cyclfrgra  28482  frgranbnb  28484  frgrawopreglem3  28509  frg2woteqm  28522  usg2spot2nb  28528  sgnn  28598  bnj563  29185  lcvbr3  29895  opltn0  30062  atlltn0  30178  hlrelat5N  30272  2dim  30341  ps-2  30349  islln3  30381  llnexatN  30392  4atlem11  30480  isline4N  30648  lhpex2leN  30884  cdleme48gfv  31408
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-cleq 2431  df-ne 2603
  Copyright terms: Public domain W3C validator