Theorem necom 3022

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 198   ≠ wne 2969

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2770  df-ne 2970

This theorem is referenced by:  necomi  3023  necomd  3024  0pss  4239  disjtp2  4483  difprsn1  4562  difprsn2  4563  prproe  4669  fndmdifcom  6585  fvpr1  6727  fvpr2  6728  fvpr1g  6729  fvtp1  6732  fvtp2  6733  fvtp3  6734  fvtp1g  6735  fvtp2g  6736  fvtp3g  6737  dff14b  6800  f12dfv  6801  f13dfv  6802  orduniorsuc  7308  kmlem3  9309  kmlem4  9310  ac6num  9636  leltne  10466  nn0lt2  11792  xrleltne  12288  fzofzim  12834  elfznelfzo  12892  elfznelfzob  12893  fleqceilz  12972  hashdifpr  13517  hashgt12el  13524  hashgt12el2  13525  cshw0  13945  cshwn  13948  isprm2lem  15799  prm2orodd  15809  cshwsdisj  16204  sgrp2nmndlem5  17803  f1omvdconj  18249  pmtrprfv3  18257  pmtr3ncomlem1  18276  dmdprdd  18785  xrsdsreclblem  20188  xrsdsreclb  20189  ordthaus  21596  hmphindis  22009  angpined  25008  funvtxval0  26363  snstrvtxval  26385  snstriedgval  26386  nbgrsym  26710  nb3grprlem2  26729  nb3grpr  26730  cusgredg  26772  cplgr3v  26783  1egrvtxdg0  26859  usgr2pthlem  27115  usgr2pth0  27117  2pthdlem1  27310  clwlkclwwlklem2a4  27377  uhgr3cyclex  27585  eupth2lem3lem4  27635  frcond1  27674  frcond4  27678  frgr3v  27683  3vfriswmgr  27686  2pthfrgr  27692  3cyclfrgrrn1  27693  n4cyclfrgr  27699  frgrnbnb  27701  frgrwopreglem4a  27718  ch0pss  28876  pmtrprfv2  30446  esumcvgre  30751  bnj563  31412  cvmsdisj  31851  nosgnn0  32400  noextendlt  32411  nosepne  32420  nosepdm  32423  nosupbnd2lem1  32450  noetalem3  32454  btwnouttr  32720  fscgr  32776  linecom  32846  linerflx2  32847  poimirlem25  34060  divrngidl  34451  lcvbr3  35177  opltn0  35344  atlltn0  35460  2dim  35624  ps-2  35632  islln3  35664  llnexatN  35675  4atlem11  35763  isline4N  35931  lhpex2leN  36167  cdleme48gfv  36691  icccncfext  41028  fourierdlem42  41293  icceuelpartlem  42403  paireqne  42450  oddprmALTV  42623  rrx2pnedifcoorneor  43452  rrx2linest  43478