Theorem necom 3071

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 208   ≠ wne 3018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-ne 3019

This theorem is referenced by:  necomi  3072  necomd  3073  0pss  4398  disjtp2  4654  difprsn1  4735  difprsn2  4736  prproe  4838  fndmdifcom  6815  fvpr1  6954  fvpr2  6955  fvpr1g  6956  fvtp1  6959  fvtp2  6960  fvtp3  6961  fvtp1g  6962  fvtp2g  6963  fvtp3g  6964  dff14b  7031  f12dfv  7032  f13dfv  7033  orduniorsuc  7547  kmlem3  9580  kmlem4  9581  ac6num  9903  leltne  10732  nn0lt2  12048  xrleltne  12541  fzofzim  13087  elfznelfzo  13145  elfznelfzob  13146  fleqceilz  13225  hashdifpr  13779  hashgt12el  13786  hashgt12el2  13787  hashgt23el  13788  cshw0  14158  cshwn  14161  isprm2lem  16027  prm2orodd  16037  cshwsdisj  16434  sgrp2nmndlem5  18096  f1omvdconj  18576  pmtrprfv3  18584  pmtr3ncomlem1  18603  dmdprdd  19123  xrsdsreclblem  20593  xrsdsreclb  20594  ordthaus  21994  hmphindis  22407  angpined  25410  funvtxval0  26802  snstrvtxval  26824  snstriedgval  26825  nbgrsym  27147  nb3grprlem2  27165  nb3grpr  27166  cusgredg  27208  cplgr3v  27219  1egrvtxdg0  27295  usgr2pthlem  27546  usgr2pth0  27548  2pthdlem1  27711  clwlkclwwlklem2a4  27777  uhgr3cyclex  27963  eupth2lem3lem4  28012  frcond1  28047  frcond4  28051  frgr3v  28056  3vfriswmgr  28059  2pthfrgr  28065  3cyclfrgrrn1  28066  n4cyclfrgr  28072  frgrnbnb  28074  frgrwopreglem4a  28091  ch0pss  29224  pmtrprfv2  30734  esumcvgre  31352  bnj563  32016  cusgredgex2  32371  cvmsdisj  32519  fmlaomn0  32639  ex-sategoelel  32670  nosgnn0  33167  noextendlt  33178  nosepne  33187  nosepdm  33190  nosupbnd2lem1  33217  noetalem3  33221  btwnouttr  33487  fscgr  33543  linecom  33613  linerflx2  33614  poimirlem25  34919  divrngidl  35308  lcvbr3  36161  opltn0  36328  atlltn0  36444  2dim  36608  ps-2  36616  islln3  36648  llnexatN  36659  4atlem11  36747  isline4N  36915  lhpex2leN  37151  cdleme48gfv  37675  pr2eldif2  39921  icccncfext  42177  fourierdlem42  42441  icceuelpartlem  43602  ichnreuop  43641  paireqne  43680  oddprmALTV  43859  rrx2pnedifcoorneor  44710  rrx2linest  44736