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

Theorem necom 2680
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 2438 . 2  |-  ( A  =  B  <->  B  =  A )
21necon3bii 2631 1  |-  ( A  =/=  B  <->  B  =/=  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    =/= wne 2599
This theorem is referenced by:  necomi  2681  necomd  2682  0pss  3658  difprsn1  3928  difprsn2  3929  diftpsn3  3930  orduniorsuc  4803  fndmdifcom  5828  fvpr1  5928  fvpr2  5929  fvpr1g  5930  fvtp1  5932  fvtp2  5933  fvtp3  5934  fvtp1g  5935  fvtp2g  5936  fvtp3g  5937  0neqopab  6112  wemapso2lem  7512  kmlem3  8025  kmlem4  8026  ac6num  8352  leltne  9157  xrleltne  10731  xrltlen  10732  fzm1  11120  elfznelfzo  11185  elfznelfzob  11186  hashgt12el  11675  hashgt12el2  11676  isprm3  13081  dmdprdd  15553  lspsncv0  16211  xrsdsreclblem  16737  xrsdsreclb  16738  ordthaus  17441  hmphindis  17822  trfbas  17869  fbunfip  17894  trfil2  17912  iundisj2  19436  angpined  20664  nb3graprlem2  21454  nb3grapr  21455  cusgra3v  21466  usgrcyclnl2  21621  constr3lem6  21629  eupath2lem3  21694  ch0pss  22940  iundisj2f  24023  iundisj2fi  24146  cvmsdisj  24950  cvmscld  24953  nosgnn0  25606  nodenselem4  25632  btwnouttr  25951  fscgr  26007  linecom  26077  linerflx2  26078  divrngidl  26630  prtlem90  26698  cmpfiiin  26743  uvcvv0  27208  f1omvdconj  27358  dff14b  28066  f12dfv  28067  f13dfv  28068  cshwssizelem2  28245  cshwsdisj  28249  usgra2pthlem1  28264  usgra2pth0  28266  frgra3v  28330  3vfriswmgra  28333  2pthfrgra  28339  3cyclfrgrarn1  28340  n4cyclfrgra  28346  frgranbnb  28348  frgrawopreglem3  28373  frg2woteqm  28386  usg2spot2nb  28392  sgnn  28462  bnj563  29049  lcvbr3  29759  opltn0  29926  atlltn0  30042  hlrelat5N  30136  2dim  30205  ps-2  30213  islln3  30245  llnexatN  30256  4atlem11  30344  isline4N  30512  lhpex2leN  30748  cdleme48gfv  31272
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-cleq 2429  df-ne 2601
  Copyright terms: Public domain W3C validator