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

Theorem necom 2830
Description: Commutation of inequality. (Contributed by NM, 14-May-1999.)
Assertion
Ref Expression
necom (𝐴𝐵𝐵𝐴)

Proof of Theorem necom
StepHypRef Expression
1 eqcom 2612 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
21necon3bii 2829 1 (𝐴𝐵𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 194  wne 2775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-cleq 2598  df-ne 2777
This theorem is referenced by:  necomi  2831  necomd  2832  0pss  3960  difprsn1  4266  difprsn2  4267  diftpsn3OLD  4269  fndmdifcom  6211  fvpr1  6335  fvpr2  6336  fvpr1g  6337  fvtp1  6339  fvtp2  6340  fvtp3  6341  fvtp1g  6342  fvtp2g  6343  fvtp3g  6344  dff14b  6402  f12dfv  6403  f13dfv  6404  orduniorsuc  6895  kmlem3  8830  kmlem4  8831  ac6num  9157  leltne  9974  nn0lt2  11269  xrleltne  11809  fzofzim  12333  elfznelfzo  12390  elfznelfzob  12391  fleqceilz  12466  hashdifpr  13012  hashgt12el  13018  hashgt12el2  13019  cshw0  13333  cshwn  13336  prm2orodd  15184  cshwsdisj  15585  sgrp2nmndlem5  17181  f1omvdconj  17631  pmtrprfv3  17639  pmtr3ncomlem1  17658  dmdprdd  18163  xrsdsreclblem  19553  xrsdsreclb  19554  ordthaus  20936  hmphindis  21348  angpined  24270  nb3graprlem2  25743  nb3grapr  25744  cusgra3v  25755  usgrcyclnl2  25931  constr3lem6  25939  clwlkisclwwlklem2a4  26074  eupath2lem3  26268  frgra3v  26291  3vfriswmgra  26294  2pthfrgra  26300  3cyclfrgrarn1  26301  n4cyclfrgra  26307  frgranbnb  26309  frg2woteqm  26348  ch0pss  27490  pmtrprfv2  28981  esumcvgre  29282  bnj563  29869  cvmsdisj  30308  nosgnn0  30857  nodenselem4  30885  btwnouttr  31103  fscgr  31159  linecom  31229  linerflx2  31230  poimirlem25  32403  divrngidl  32796  lcvbr3  33127  opltn0  33294  atlltn0  33410  2dim  33573  ps-2  33581  islln3  33613  llnexatN  33624  4atlem11  33712  isline4N  33880  lhpex2leN  34116  cdleme48gfv  34642  icccncfext  38573  fourierdlem42  38842  icceuelpartlem  39774  oddprmALTV  39937  funvtxval0  40244  snstrvtxval  40266  snstriedgval  40267  nbgrsym  40589  nb3grprlem2  40607  nb3grpr  40608  cusgredg  40644  cplgr3v  40655  1egrvtxdg0  40725  usgr2pthlem  40967  usgr2pth0  40969  2pthdlem1  41135  clwlkclwwlklem2a4  41204  uhgr3cyclex  41347  eupth2lem3lem4  41397  frcond1  41436  frgr3v  41443  3vfriswmgr  41446  2pthfrgr  41452  3cyclfrgrrn1  41453  n4cyclfrgr  41459  frgrnbnb  41461
  Copyright terms: Public domain W3C validator