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

Theorem necom 2994
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 2993 1 (𝐴𝐵𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wne 2940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ne 2941
This theorem is referenced by:  necomi  2995  necomd  2996  dfdif3  4117  0pss  4447  iftrueb  4538  disjtp2  4716  difprsn1  4800  difprsn2  4801  prproe  4905  fndmdifcom  7063  fvpr1g  7210  fvpr2g  7211  fvtp1  7215  fvtp2  7216  fvtp3  7217  fvtp1g  7218  fvtp2g  7219  fvtp3g  7220  dff14b  7291  f12dfv  7293  f13dfv  7294  orduniorsuc  7850  kmlem3  10193  kmlem4  10194  ac6num  10519  leltne  11350  nn0lt2  12681  xrleltne  13187  fzofzim  13749  elfznelfzo  13811  elfznelfzob  13812  fleqceilz  13894  hashdifpr  14454  hashgt12el  14461  hashgt12el2  14462  hashgt23el  14463  hash7g  14525  cshw0  14832  cshwn  14835  isprm2lem  16718  prm2orodd  16728  cshwsdisj  17136  sgrp2nmndlem5  18942  f1omvdconj  19464  pmtrprfv3  19472  pmtr3ncomlem1  19491  dmdprdd  20019  cnfldfunALT  21379  cnfldfunALTOLD  21392  xrsdsreclblem  21430  xrsdsreclb  21431  ordthaus  23392  hmphindis  23805  angpined  26873  nosgnn0  27703  noextendlt  27714  nosepne  27725  nosepdm  27729  nosupbnd2lem1  27760  noinfbnd2lem1  27775  noetasuplem4  27781  funvtxval0  29032  snstrvtxval  29054  snstriedgval  29055  nbgrsym  29380  nb3grprlem2  29398  nb3grpr  29399  cusgredg  29441  cplgr3v  29452  1egrvtxdg0  29529  usgr2pthlem  29783  usgr2pth0  29785  2pthdlem1  29950  clwlkclwwlklem2a4  30016  uhgr3cyclex  30201  eupth2lem3lem4  30250  frcond1  30285  frcond4  30289  frgr3v  30294  3vfriswmgr  30297  2pthfrgr  30303  3cyclfrgrrn1  30304  n4cyclfrgr  30310  frgrnbnb  30312  frgrwopreglem4a  30329  ch0pss  31464  pmtrprfv2  33108  esumcvgre  34092  bnj563  34757  cusgredgex2  35128  cvmsdisj  35275  fmlaomn0  35395  ex-sategoelel  35426  btwnouttr  36025  fscgr  36081  linecom  36151  linerflx2  36152  poimirlem25  37652  divrngidl  38035  lcvbr3  39024  opltn0  39191  atlltn0  39307  2dim  39472  ps-2  39480  islln3  39512  llnexatN  39523  4atlem11  39611  isline4N  39779  lhpex2leN  40015  cdleme48gfv  40539  60gcd7e1  42006  dvrelogpow2b  42069  aks4d1p1p4  42072  aks6d1c2p2  42120  fsuppind  42600  onov0suclim  43287  oenassex  43331  pr2eldif2  43568  pimxrneun  45499  icccncfext  45902  fourierdlem42  46164  icceuelpartlem  47422  ichnreuop  47459  paireqne  47498  oddprmALTV  47674  rrx2pnedifcoorneor  48637  rrx2linest  48663
  Copyright terms: Public domain W3C validator