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

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

Proof of Theorem necom
StepHypRef Expression
1 eqcom 2658 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
21necon3bii 2875 1 (𝐴𝐵𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wne 2823
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-ne 2824
This theorem is referenced by:  necomi  2877  necomd  2878  0pss  4046  disjtp2  4284  difprsn1  4362  difprsn2  4363  diftpsn3OLD  4365  prproe  4466  fndmdifcom  6362  fvpr1  6497  fvpr2  6498  fvpr1g  6499  fvtp1  6501  fvtp2  6502  fvtp3  6503  fvtp1g  6504  fvtp2g  6505  fvtp3g  6506  dff14b  6568  f12dfv  6569  f13dfv  6570  orduniorsuc  7072  kmlem3  9012  kmlem4  9013  ac6num  9339  leltne  10165  nn0lt2  11478  xrleltne  12016  fzofzim  12554  elfznelfzo  12613  elfznelfzob  12614  fleqceilz  12693  hashdifpr  13241  hashgt12el  13248  hashgt12el2  13249  cshw0  13586  cshwn  13589  isprm2lem  15441  prm2orodd  15451  cshwsdisj  15852  sgrp2nmndlem5  17463  f1omvdconj  17912  pmtrprfv3  17920  pmtr3ncomlem1  17939  dmdprdd  18444  xrsdsreclblem  19840  xrsdsreclb  19841  ordthaus  21236  hmphindis  21648  angpined  24602  funvtxval0  25942  funvtxval0OLD  25943  snstrvtxval  25974  snstriedgval  25975  nbgrsym  26308  nbgrsymOLD  26309  nb3grprlem2  26327  nb3grpr  26328  cusgredg  26376  cplgr3v  26387  1egrvtxdg0  26463  usgr2pthlem  26715  usgr2pth0  26717  2pthdlem1  26895  clwlkclwwlklem2a4  26963  uhgr3cyclex  27160  eupth2lem3lem4  27209  frcond1  27246  frcond4  27250  frgr3v  27255  3vfriswmgr  27258  2pthfrgr  27264  3cyclfrgrrn1  27265  n4cyclfrgr  27271  frgrnbnb  27273  frgrwopreglem4a  27290  ch0pss  28432  pmtrprfv2  29976  esumcvgre  30281  bnj563  30939  cvmsdisj  31378  nosgnn0  31936  noextendlt  31947  nosepne  31956  nosepdm  31959  nosupbnd2lem1  31986  noetalem3  31990  btwnouttr  32256  fscgr  32312  linecom  32382  linerflx2  32383  poimirlem25  33564  divrngidl  33957  lcvbr3  34628  opltn0  34795  atlltn0  34911  2dim  35074  ps-2  35082  islln3  35114  llnexatN  35125  4atlem11  35213  isline4N  35381  lhpex2leN  35617  cdleme48gfv  36142  icccncfext  40418  fourierdlem42  40684  icceuelpartlem  41696  oddprmALTV  41923
  Copyright terms: Public domain W3C validator