Theorem necom 2835

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 195   ≠ wne 2780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782

This theorem is referenced by:  necomi  2836  necomd  2837  0pss  3965  difprsn1  4271  difprsn2  4272  diftpsn3OLD  4274  fndmdifcom  6230  fvpr1  6361  fvpr2  6362  fvpr1g  6363  fvtp1  6365  fvtp2  6366  fvtp3  6367  fvtp1g  6368  fvtp2g  6369  fvtp3g  6370  dff14b  6428  f12dfv  6429  f13dfv  6430  orduniorsuc  6922  kmlem3  8857  kmlem4  8858  ac6num  9184  leltne  10006  nn0lt2  11317  xrleltne  11854  fzofzim  12382  elfznelfzo  12439  elfznelfzob  12440  fleqceilz  12515  hashdifpr  13064  hashgt12el  13070  hashgt12el2  13071  cshw0  13391  cshwn  13394  prm2orodd  15242  cshwsdisj  15643  sgrp2nmndlem5  17239  f1omvdconj  17689  pmtrprfv3  17697  pmtr3ncomlem1  17716  dmdprdd  18221  xrsdsreclblem  19611  xrsdsreclb  19612  ordthaus  20998  hmphindis  21410  angpined  24357  funvtxval0  25690  snstrvtxval  25712  snstriedgval  25713  nb3graprlem2  25981  nb3grapr  25982  cusgra3v  25993  usgrcyclnl2  26169  constr3lem6  26177  clwlkisclwwlklem2a4  26312  eupath2lem3  26506  frgra3v  26529  3vfriswmgra  26532  2pthfrgra  26538  3cyclfrgrarn1  26539  n4cyclfrgra  26545  frgranbnb  26547  frg2woteqm  26586  ch0pss  27688  pmtrprfv2  29179  esumcvgre  29480  bnj563  30067  cvmsdisj  30506  nosgnn0  31055  nodenselem4  31083  btwnouttr  31301  fscgr  31357  linecom  31427  linerflx2  31428  poimirlem25  32604  divrngidl  32997  lcvbr3  33328  opltn0  33495  atlltn0  33611  2dim  33774  ps-2  33782  islln3  33814  llnexatN  33825  4atlem11  33913  isline4N  34081  lhpex2leN  34317  cdleme48gfv  34843  icccncfext  38773  fourierdlem42  39042  icceuelpartlem  39973  oddprmALTV  40136  nbgrsym  40591  nb3grprlem2  40609  nb3grpr  40610  cusgredg  40646  cplgr3v  40657  1egrvtxdg0  40727  usgr2pthlem  40969  usgr2pth0  40971  2pthdlem1  41137  clwlkclwwlklem2a4  41206  uhgr3cyclex  41349  eupth2lem3lem4  41399  frcond1  41438  frgr3v  41445  3vfriswmgr  41448  2pthfrgr  41454  3cyclfrgrrn1  41455  n4cyclfrgr  41461  frgrnbnb  41463