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

Theorem necom 2540
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 2298 . 2  |-  ( A  =  B  <->  B  =  A )
21necon3bii 2491 1  |-  ( A  =/=  B  <->  B  =/=  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    =/= wne 2459
This theorem is referenced by:  necomi  2541  necomd  2542  0pss  3505  difprsn1  3770  difprsn2  3771  diftpsn3  3772  orduniorsuc  4637  fndmdifcom  5646  fvpr1  5738  fvpr2  5739  fvtp1  5740  fvtp2  5741  fvtp3  5742  wemapso2lem  7281  kmlem3  7794  kmlem4  7795  ac6num  8122  leltne  8927  xrleltne  10495  xrltlen  10496  fzm1  10878  isprm3  12783  dmdprdd  15253  lspsncv0  15915  xrsdsreclblem  16433  xrsdsreclb  16434  ordthaus  17128  hmphindis  17504  trfbas  17555  fbunfip  17580  trfil2  17598  iundisj2  18922  angpined  20143  ch0pss  22040  iundisj2fi  23379  iundisj2f  23381  cvmsdisj  23816  cvmscld  23819  eupath2lem3  23918  nosgnn0  24383  nodenselem4  24409  btwnouttr  24719  fscgr  24775  linecom  24845  linerflx2  24846  repcpwti  25264  lineval4a  26190  lppotos  26247  dfcon2OLD  26356  divrngidl  26756  prtlem90  26826  cmpfiiin  26875  uvcvv0  27342  f1omvdconj  27492  0neqopab  28192  elfznelfzo  28213  hashgt12el  28218  hashgt12el2  28219  nb3graprlem2  28288  nb3grapr  28289  cusgra2v  28297  cusgra3v  28299  usgrcyclnl2  28387  constr3lem4  28393  constr3lem6  28395  frgra2v  28423  frgra3v  28426  3vfriswmgra  28429  3cyclfrgrarn1  28435  n4cyclfrgra  28440  sgnn  28505  bnj563  29088  lcvbr3  29835  opltn0  30002  atlltn0  30118  hlrelat5N  30212  2dim  30281  ps-2  30289  islln3  30321  llnexatN  30332  4atlem11  30420  isline4N  30588  lhpex2leN  30824  cdleme48gfv  31348
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289  df-ne 2461
  Copyright terms: Public domain W3C validator