Theorem necom 2991

Description: Commutation of inequality. (Contributed by NM, 14-May-1999.)

Assertion

Ref	Expression
necom	⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)

Proof of Theorem necom

Step	Hyp	Ref	Expression
1		eqcom 2741	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
2	1	necon3bii 2990	1 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)

Syntax hints:   ↔ wb 206   ≠ wne 2937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ne 2938

This theorem is referenced by:  necomi  2992  necomd  2993  dfdif3  4126  0pss  4452  disjtp2  4720  difprsn1  4804  difprsn2  4805  prproe  4909  fndmdifcom  7062  fvpr1g  7209  fvpr2g  7210  fvtp1  7214  fvtp2  7215  fvtp3  7216  fvtp1g  7217  fvtp2g  7218  fvtp3g  7219  dff14b  7290  f12dfv  7292  f13dfv  7293  orduniorsuc  7849  kmlem3  10190  kmlem4  10191  ac6num  10516  leltne  11347  nn0lt2  12678  xrleltne  13183  fzofzim  13745  elfznelfzo  13807  elfznelfzob  13808  fleqceilz  13890  hashdifpr  14450  hashgt12el  14457  hashgt12el2  14458  hashgt23el  14459  hash7g  14521  cshw0  14828  cshwn  14831  isprm2lem  16714  prm2orodd  16724  cshwsdisj  17132  sgrp2nmndlem5  18954  f1omvdconj  19478  pmtrprfv3  19486  pmtr3ncomlem1  19505  dmdprdd  20033  cnfldfunALT  21396  cnfldfunALTOLD  21409  xrsdsreclblem  21447  xrsdsreclb  21448  ordthaus  23407  hmphindis  23820  angpined  26887  nosgnn0  27717  noextendlt  27728  nosepne  27739  nosepdm  27743  nosupbnd2lem1  27774  noinfbnd2lem1  27789  noetasuplem4  27795  funvtxval0  29046  snstrvtxval  29068  snstriedgval  29069  nbgrsym  29394  nb3grprlem2  29412  nb3grpr  29413  cusgredg  29455  cplgr3v  29466  1egrvtxdg0  29543  usgr2pthlem  29795  usgr2pth0  29797  2pthdlem1  29959  clwlkclwwlklem2a4  30025  uhgr3cyclex  30210  eupth2lem3lem4  30259  frcond1  30294  frcond4  30298  frgr3v  30303  3vfriswmgr  30306  2pthfrgr  30312  3cyclfrgrrn1  30313  n4cyclfrgr  30319  frgrnbnb  30321  frgrwopreglem4a  30338  ch0pss  31473  pmtrprfv2  33090  esumcvgre  34071  bnj563  34735  cusgredgex2  35106  cvmsdisj  35254  fmlaomn0  35374  ex-sategoelel  35405  btwnouttr  36005  fscgr  36061  linecom  36131  linerflx2  36132  poimirlem25  37631  divrngidl  38014  lcvbr3  39004  opltn0  39171  atlltn0  39287  2dim  39452  ps-2  39460  islln3  39492  llnexatN  39503  4atlem11  39591  isline4N  39759  lhpex2leN  39995  cdleme48gfv  40519  60gcd7e1  41986  dvrelogpow2b  42049  aks4d1p1p4  42052  aks6d1c2p2  42100  fsuppind  42576  onov0suclim  43263  oenassex  43307  pr2eldif2  43544  pimxrneun  45438  icccncfext  45842  fourierdlem42  46104  icceuelpartlem  47359  ichnreuop  47396  paireqne  47435  oddprmALTV  47611  rrx2pnedifcoorneor  48565  rrx2linest  48591