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

Theorem necom 2527
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 2285 . 2  |-  ( A  =  B  <->  B  =  A )
21necon3bii 2478 1  |-  ( A  =/=  B  <->  B  =/=  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    =/= wne 2446
This theorem is referenced by:  necomi  2528  necomd  2529  0pss  3492  orduniorsuc  4621  fndmdifcom  5630  fvpr1  5722  fvpr2  5723  fvtp1  5724  fvtp2  5725  fvtp3  5726  wemapso2lem  7265  kmlem3  7778  kmlem4  7779  ac6num  8106  leltne  8911  xrleltne  10479  xrltlen  10480  fzm1  10862  isprm3  12767  dmdprdd  15237  lspsncv0  15899  xrsdsreclblem  16417  xrsdsreclb  16418  ordthaus  17112  hmphindis  17488  trfbas  17539  fbunfip  17564  trfil2  17582  iundisj2  18906  angpined  20127  ch0pss  22024  difprsn2  23191  iundisj2fi  23364  iundisj2f  23366  cvmsdisj  23801  cvmscld  23804  eupath2lem3  23903  nosgnn0  24312  nodenselem4  24338  btwnouttr  24647  fscgr  24703  linecom  24773  linerflx2  24774  repcpwti  25161  lineval4a  26087  lppotos  26144  dfcon2OLD  26253  divrngidl  26653  prtlem90  26723  cmpfiiin  26772  uvcvv0  27239  f1omvdconj  27389  diftpsneq  28070  cusgra2v  28158  frgra2v  28177  frgra3v  28180  3vfriswmgra  28183  sgnn  28251  bnj563  28772  lcvbr3  29213  opltn0  29380  atlltn0  29496  hlrelat5N  29590  2dim  29659  ps-2  29667  islln3  29699  llnexatN  29710  4atlem11  29798  isline4N  29966  lhpex2leN  30202  cdleme48gfv  30726
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276  df-ne 2448
  Copyright terms: Public domain W3C validator