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

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

Proof of Theorem necom
StepHypRef Expression
1 eqcom 2627 . 2 (𝐴 = 𝐵𝐵 = 𝐴)
21necon3bii 2843 1 (𝐴𝐵𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wne 2791
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-cleq 2613  df-ne 2792
This theorem is referenced by:  necomi  2845  necomd  2846  0pss  4004  disjtp2  4243  difprsn1  4321  difprsn2  4322  diftpsn3OLD  4324  prproe  4425  fndmdifcom  6308  fvpr1  6441  fvpr2  6442  fvpr1g  6443  fvtp1  6445  fvtp2  6446  fvtp3  6447  fvtp1g  6448  fvtp2g  6449  fvtp3g  6450  dff14b  6513  f12dfv  6514  f13dfv  6515  orduniorsuc  7015  kmlem3  8959  kmlem4  8960  ac6num  9286  leltne  10112  nn0lt2  11425  xrleltne  11963  fzofzim  12498  elfznelfzo  12557  elfznelfzob  12558  fleqceilz  12636  hashdifpr  13186  hashgt12el  13193  hashgt12el2  13194  cshw0  13521  cshwn  13524  prm2orodd  15385  cshwsdisj  15786  sgrp2nmndlem5  17397  f1omvdconj  17847  pmtrprfv3  17855  pmtr3ncomlem1  17874  dmdprdd  18379  xrsdsreclblem  19773  xrsdsreclb  19774  ordthaus  21169  hmphindis  21581  angpined  24538  funvtxval0  25878  funvtxval0OLD  25879  snstrvtxval  25910  snstriedgval  25911  nbgrsym  26246  nb3grprlem2  26264  nb3grpr  26265  cusgredg  26301  cplgr3v  26312  1egrvtxdg0  26388  usgr2pthlem  26640  usgr2pth0  26642  2pthdlem1  26807  clwlkclwwlklem2a4  26879  uhgr3cyclex  27022  eupth2lem3lem4  27071  frcond1  27110  frcond4  27114  frgr3v  27119  3vfriswmgr  27122  2pthfrgr  27128  3cyclfrgrrn1  27129  n4cyclfrgr  27135  frgrnbnb  27137  ch0pss  28274  pmtrprfv2  29822  esumcvgre  30127  bnj563  30787  cvmsdisj  31226  nosgnn0  31785  noextendlt  31796  nosepne  31805  nosepdm  31808  nosupbnd2lem1  31835  noetalem3  31839  btwnouttr  32106  fscgr  32162  linecom  32232  linerflx2  32233  poimirlem25  33405  divrngidl  33798  lcvbr3  34129  opltn0  34296  atlltn0  34412  2dim  34575  ps-2  34583  islln3  34615  llnexatN  34626  4atlem11  34714  isline4N  34882  lhpex2leN  35118  cdleme48gfv  35644  icccncfext  39863  fourierdlem42  40129  icceuelpartlem  41135  oddprmALTV  41363
  Copyright terms: Public domain W3C validator