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

Theorem necom 2648
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 2406 . 2  |-  ( A  =  B  <->  B  =  A )
21necon3bii 2599 1  |-  ( A  =/=  B  <->  B  =/=  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    =/= wne 2567
This theorem is referenced by:  necomi  2649  necomd  2650  0pss  3625  difprsn1  3895  difprsn2  3896  diftpsn3  3897  orduniorsuc  4769  fndmdifcom  5794  fvpr1  5894  fvpr2  5895  fvpr1g  5896  fvtp1  5898  fvtp2  5899  fvtp3  5900  fvtp1g  5901  fvtp2g  5902  fvtp3g  5903  0neqopab  6078  wemapso2lem  7475  kmlem3  7988  kmlem4  7989  ac6num  8315  leltne  9120  xrleltne  10694  xrltlen  10695  fzm1  11082  elfznelfzo  11147  elfznelfzob  11148  hashgt12el  11637  hashgt12el2  11638  isprm3  13043  dmdprdd  15515  lspsncv0  16173  xrsdsreclblem  16699  xrsdsreclb  16700  ordthaus  17402  hmphindis  17782  trfbas  17829  fbunfip  17854  trfil2  17872  iundisj2  19396  angpined  20624  nb3graprlem2  21414  nb3grapr  21415  cusgra3v  21426  usgrcyclnl2  21581  constr3lem6  21589  eupath2lem3  21654  ch0pss  22900  iundisj2f  23983  iundisj2fi  24106  cvmsdisj  24910  cvmscld  24913  nosgnn0  25526  nodenselem4  25552  btwnouttr  25862  fscgr  25918  linecom  25988  linerflx2  25989  divrngidl  26528  prtlem90  26596  cmpfiiin  26641  uvcvv0  27107  f1omvdconj  27257  dff14b  27960  f12dfv  27961  f13dfv  27962  usgra2pthlem1  28040  usgra2pth0  28042  frgra3v  28106  3vfriswmgra  28109  2pthfrgra  28115  3cyclfrgrarn1  28116  n4cyclfrgra  28122  frgranbnb  28124  frgrawopreglem3  28149  frg2woteqm  28162  usg2spot2nb  28168  sgnn  28238  bnj563  28817  lcvbr3  29506  opltn0  29673  atlltn0  29789  hlrelat5N  29883  2dim  29952  ps-2  29960  islln3  29992  llnexatN  30003  4atlem11  30091  isline4N  30259  lhpex2leN  30495  cdleme48gfv  31019
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-cleq 2397  df-ne 2569
  Copyright terms: Public domain W3C validator