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

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

Proof of Theorem necom
StepHypRef Expression
1 eqcom 2744 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
21necon3bii 2997 1 (𝐴𝐵𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wne 2944
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729  df-ne 2945
This theorem is referenced by:  necomi  2999  necomd  3000  0pss  4409  disjtp2  4682  difprsn1  4765  difprsn2  4766  prproe  4868  fndmdifcom  6998  fvpr1g  7141  fvpr2g  7142  fvpr1OLD  7145  fvpr2OLD  7147  fvtp1  7149  fvtp2  7150  fvtp3  7151  fvtp1g  7152  fvtp2g  7153  fvtp3g  7154  dff14b  7223  f12dfv  7224  f13dfv  7225  orduniorsuc  7770  kmlem3  10095  kmlem4  10096  ac6num  10422  leltne  11251  nn0lt2  12573  xrleltne  13071  fzofzim  13626  elfznelfzo  13684  elfznelfzob  13685  fleqceilz  13766  hashdifpr  14322  hashgt12el  14329  hashgt12el2  14330  hashgt23el  14331  cshw0  14689  cshwn  14692  isprm2lem  16564  prm2orodd  16574  cshwsdisj  16978  sgrp2nmndlem5  18746  f1omvdconj  19235  pmtrprfv3  19243  pmtr3ncomlem1  19262  dmdprdd  19785  cnfldfunALT  20825  xrsdsreclblem  20859  xrsdsreclb  20860  ordthaus  22751  hmphindis  23164  angpined  26196  nosgnn0  27022  noextendlt  27033  nosepne  27044  nosepdm  27048  nosupbnd2lem1  27079  noinfbnd2lem1  27094  noetasuplem4  27100  funvtxval0  28008  snstrvtxval  28030  snstriedgval  28031  nbgrsym  28353  nb3grprlem2  28371  nb3grpr  28372  cusgredg  28414  cplgr3v  28425  1egrvtxdg0  28501  usgr2pthlem  28753  usgr2pth0  28755  2pthdlem1  28917  clwlkclwwlklem2a4  28983  uhgr3cyclex  29168  eupth2lem3lem4  29217  frcond1  29252  frcond4  29256  frgr3v  29261  3vfriswmgr  29264  2pthfrgr  29270  3cyclfrgrrn1  29271  n4cyclfrgr  29277  frgrnbnb  29279  frgrwopreglem4a  29296  ch0pss  30429  pmtrprfv2  31981  esumcvgre  32730  bnj563  33395  cusgredgex2  33756  cvmsdisj  33904  fmlaomn0  34024  ex-sategoelel  34055  btwnouttr  34638  fscgr  34694  linecom  34764  linerflx2  34765  poimirlem25  36132  divrngidl  36516  lcvbr3  37514  opltn0  37681  atlltn0  37797  2dim  37962  ps-2  37970  islln3  38002  llnexatN  38013  4atlem11  38101  isline4N  38269  lhpex2leN  38505  cdleme48gfv  39029  60gcd7e1  40491  dvrelogpow2b  40554  aks4d1p1p4  40557  aks6d1c2p2  40578  fsuppind  40794  onov0suclim  41638  oenassex  41682  pr2eldif2  41901  pimxrneun  43798  icccncfext  44202  fourierdlem42  44464  icceuelpartlem  45701  ichnreuop  45738  paireqne  45777  oddprmALTV  45953  rrx2pnedifcoorneor  46876  rrx2linest  46902
  Copyright terms: Public domain W3C validator