Theorem necom 3008

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

Assertion

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

Proof of Theorem necom

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

This proof depends on syntax axioms:   ↔ wb 209   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ne 2956

This theorem is used by:  necomi  3009  necomd  3010  dfdif3  4055  0pss  4359  iftrueb  4494  disjtp2  4673  difprsn1  4759  difprsn2  4760  prproe  4832  fndmdifcom  7043  fvpr1g  7196  fvpr2g  7197  fvtp1  7201  fvtp2  7202  fvtp3  7203  fvtp1g  7204  fvtp2g  7205  fvtp3g  7206  dff14b  7276  f12dfv  7282  f13dfv  7283  orduniorsuc  7842  onelfvnef1  8453  kmlem3  10235  kmlem4  10236  ac6num  10561  leltne  11403  nn0lt2  12766  xrleltne  13278  fzofzim  13848  elfznelfzo  13912  elfznelfzob  13913  fleqceilz  13998  hashdifpr  14564  hashgt12el  14571  hashgt12el2  14572  hashgt23el  14573  hash7g  14635  cshw0  14950  cshwn  14953  isprm2lem  16862  prm2orodd  16872  cshwsdisj  17282  sgrp2nmndlem5  19134  f1omvdconj  19666  pmtrprfv3  19674  pmtr3ncomlem1  19693  dmdprdd  20221  cnfldfunALT  21699  xrsdsreclblem  21725  xrsdsreclb  21726  ordthaus  23708  hmphindis  24122  angpined  27164  nosgnn0  28021  noextendlt  28032  nosepne  28043  nosepdm  28047  nosupbnd2lem1  28078  noinfbnd2lem1  28093  noetasuplem4  28099  funvtxval0  29599  snstrvtxval  29621  snstriedgval  29622  nbgrsym  29950  nb3grprlem2  29968  nb3grpr  29969  cusgredg  30011  cplgr3v  30022  1egrvtxdg0  30098  usgr2pthlem  30355  usgr2pth0  30357  2pthdlem1  30525  clwlkclwwlklem2a4  30594  uhgr3cyclex  30789  eupth2lem3lem4  30838  frcond1  30873  frcond4  30877  frgr3v  30882  3vfriswmgr  30885  2pthfrgr  30891  3cyclfrgrrn1  30892  n4cyclfrgr  30898  frgrnbnb  30900  frgrwopreglem4a  30917  ch0pss  32053  pmtrprfv2  33696  esumcvgre  34770  bnj563  35421  cusgredgex2  35984  cvmsdisj  36122  fmlaomn0  36242  ex-sategoelel  36273  btwnouttr  36882  fscgr  36938  linecom  37008  linerflx2  37009  poimirlem25  38657  divrngidl  39056  lcvbr3  40174  opltn0  40341  atlltn0  40457  2dim  40621  ps-2  40629  islln3  40661  llnexatN  40672  4atlem11  40760  isline4N  40928  lhpex2leN  41164  cdleme48gfv  41688  60gcd7e1  43149  dvrelogpow2b  43212  aks4d1p1p4  43215  aks6d1c2p2  43263  fsuppind  43712  onov0suclim  44370  oenassex  44414  pr2eldif2  44650  pimxrneun  46592  icccncfext  46991  fourierdlem42  47253  sqrtnzqaa  48008  icceuelpartlem  48611  ichnreuop  48648  paireqne  48687  oddprmALTV  48879  rrx2pnedifcoorneor  49923  rrx2linest  49948