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

Theorem necom 2624
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 2382 . 2  |-  ( A  =  B  <->  B  =  A )
21necon3bii 2575 1  |-  ( A  =/=  B  <->  B  =/=  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    =/= wne 2543
This theorem is referenced by:  necomi  2625  necomd  2626  0pss  3601  difprsn1  3871  difprsn2  3872  diftpsn3  3873  orduniorsuc  4743  fndmdifcom  5767  fvpr1  5867  fvpr2  5868  fvpr1g  5869  fvtp1  5871  fvtp2  5872  fvtp3  5873  fvtp1g  5874  fvtp2g  5875  fvtp3g  5876  0neqopab  6051  wemapso2lem  7445  kmlem3  7958  kmlem4  7959  ac6num  8285  leltne  9090  xrleltne  10663  xrltlen  10664  fzm1  11050  elfznelfzo  11112  elfznelfzob  11113  hashgt12el  11602  hashgt12el2  11603  isprm3  13008  dmdprdd  15480  lspsncv0  16138  xrsdsreclblem  16660  xrsdsreclb  16661  ordthaus  17363  hmphindis  17743  trfbas  17790  fbunfip  17815  trfil2  17833  iundisj2  19303  angpined  20531  nb3graprlem2  21320  nb3grapr  21321  cusgra3v  21332  usgrcyclnl2  21469  constr3lem6  21477  eupath2lem3  21542  ch0pss  22788  iundisj2f  23866  iundisj2fi  23984  cvmsdisj  24729  cvmscld  24732  nosgnn0  25329  nodenselem4  25355  btwnouttr  25665  fscgr  25721  linecom  25791  linerflx2  25792  divrngidl  26322  prtlem90  26390  cmpfiiin  26435  uvcvv0  26901  f1omvdconj  27051  frgra3v  27748  3vfriswmgra  27751  2pthfrgra  27757  3cyclfrgrarn1  27758  n4cyclfrgra  27764  frgranbnb  27766  frgrawopreglem3  27791  sgnn  27863  bnj563  28442  lcvbr3  29189  opltn0  29356  atlltn0  29472  hlrelat5N  29566  2dim  29635  ps-2  29643  islln3  29675  llnexatN  29686  4atlem11  29774  isline4N  29942  lhpex2leN  30178  cdleme48gfv  30702
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 2361
This theorem depends on definitions:  df-bi 178  df-cleq 2373  df-ne 2545
  Copyright terms: Public domain W3C validator