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

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

Proof of Theorem necom
StepHypRef Expression
1 eqcom 2827 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
21necon3bii 3058 1 (𝐴𝐵𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 208  wne 3006
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2813  df-ne 3007
This theorem is referenced by:  necomi  3060  necomd  3061  0pss  4372  disjtp2  4628  difprsn1  4709  difprsn2  4710  prproe  4812  fndmdifcom  6789  fvpr1  6928  fvpr2  6929  fvpr1g  6930  fvtp1  6933  fvtp2  6934  fvtp3  6935  fvtp1g  6936  fvtp2g  6937  fvtp3g  6938  dff14b  7006  f12dfv  7007  f13dfv  7008  orduniorsuc  7523  kmlem3  9556  kmlem4  9557  ac6num  9879  leltne  10708  nn0lt2  12024  xrleltne  12517  fzofzim  13068  elfznelfzo  13126  elfznelfzob  13127  fleqceilz  13206  hashdifpr  13761  hashgt12el  13768  hashgt12el2  13769  hashgt23el  13770  cshw0  14136  cshwn  14139  isprm2lem  16003  prm2orodd  16013  cshwsdisj  16411  sgrp2nmndlem5  18073  f1omvdconj  18553  pmtrprfv3  18561  pmtr3ncomlem1  18580  dmdprdd  19100  xrsdsreclblem  20567  xrsdsreclb  20568  ordthaus  21968  hmphindis  22381  angpined  25395  funvtxval0  26787  snstrvtxval  26809  snstriedgval  26810  nbgrsym  27132  nb3grprlem2  27150  nb3grpr  27151  cusgredg  27193  cplgr3v  27204  1egrvtxdg0  27280  usgr2pthlem  27531  usgr2pth0  27533  2pthdlem1  27695  clwlkclwwlklem2a4  27761  uhgr3cyclex  27946  eupth2lem3lem4  27995  frcond1  28030  frcond4  28034  frgr3v  28039  3vfriswmgr  28042  2pthfrgr  28048  3cyclfrgrrn1  28049  n4cyclfrgr  28055  frgrnbnb  28057  frgrwopreglem4a  28074  ch0pss  29207  pmtrprfv2  30740  esumcvgre  31358  bnj563  32022  cusgredgex2  32377  cvmsdisj  32525  fmlaomn0  32645  ex-sategoelel  32676  nosgnn0  33173  noextendlt  33184  nosepne  33193  nosepdm  33196  nosupbnd2lem1  33223  noetalem3  33227  btwnouttr  33493  fscgr  33549  linecom  33619  linerflx2  33620  poimirlem25  34958  divrngidl  35342  lcvbr3  36195  opltn0  36362  atlltn0  36478  2dim  36642  ps-2  36650  islln3  36682  llnexatN  36693  4atlem11  36781  isline4N  36949  lhpex2leN  37185  cdleme48gfv  37709  60gcd7e1  39157  pr2eldif2  40049  icccncfext  42320  fourierdlem42  42582  icceuelpartlem  43743  ichnreuop  43780  paireqne  43819  oddprmALTV  43997  rrx2pnedifcoorneor  44890  rrx2linest  44916
  Copyright terms: Public domain W3C validator