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

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

Proof of Theorem necom
StepHypRef Expression
1 eqcom 2828 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
21necon3bii 3068 1 (𝐴𝐵𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wne 3016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-ne 3017
This theorem is referenced by:  necomi  3070  necomd  3071  0pss  4394  disjtp2  4646  difprsn1  4727  difprsn2  4728  prproe  4830  fndmdifcom  6806  fvpr1  6945  fvpr2  6946  fvpr1g  6947  fvtp1  6950  fvtp2  6951  fvtp3  6952  fvtp1g  6953  fvtp2g  6954  fvtp3g  6955  dff14b  7020  f12dfv  7021  f13dfv  7022  orduniorsuc  7533  kmlem3  9567  kmlem4  9568  ac6num  9890  leltne  10719  nn0lt2  12034  xrleltne  12528  fzofzim  13074  elfznelfzo  13132  elfznelfzob  13133  fleqceilz  13212  hashdifpr  13766  hashgt12el  13773  hashgt12el2  13774  hashgt23el  13775  cshw0  14146  cshwn  14149  isprm2lem  16015  prm2orodd  16025  cshwsdisj  16422  sgrp2nmndlem5  18034  f1omvdconj  18505  pmtrprfv3  18513  pmtr3ncomlem1  18532  dmdprdd  19052  xrsdsreclblem  20521  xrsdsreclb  20522  ordthaus  21922  hmphindis  22335  angpined  25335  funvtxval0  26728  snstrvtxval  26750  snstriedgval  26751  nbgrsym  27073  nb3grprlem2  27091  nb3grpr  27092  cusgredg  27134  cplgr3v  27145  1egrvtxdg0  27221  usgr2pthlem  27472  usgr2pth0  27474  2pthdlem1  27637  clwlkclwwlklem2a4  27703  uhgr3cyclex  27889  eupth2lem3lem4  27938  frcond1  27973  frcond4  27977  frgr3v  27982  3vfriswmgr  27985  2pthfrgr  27991  3cyclfrgrrn1  27992  n4cyclfrgr  27998  frgrnbnb  28000  frgrwopreglem4a  28017  ch0pss  29150  pmtrprfv2  30660  esumcvgre  31250  bnj563  31914  cusgredgex2  32267  cvmsdisj  32415  fmlaomn0  32535  ex-sategoelel  32566  nosgnn0  33063  noextendlt  33074  nosepne  33083  nosepdm  33086  nosupbnd2lem1  33113  noetalem3  33117  btwnouttr  33383  fscgr  33439  linecom  33509  linerflx2  33510  poimirlem25  34799  divrngidl  35189  lcvbr3  36041  opltn0  36208  atlltn0  36324  2dim  36488  ps-2  36496  islln3  36528  llnexatN  36539  4atlem11  36627  isline4N  36795  lhpex2leN  37031  cdleme48gfv  37555  pr2eldif2  39794  icccncfext  42050  fourierdlem42  42315  icceuelpartlem  43442  ichnreuop  43481  paireqne  43520  oddprmALTV  43699  rrx2pnedifcoorneor  44601  rrx2linest  44627
  Copyright terms: Public domain W3C validator