Theorem necom 3010

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

Assertion

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

Proof of Theorem necom

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-ne 2958

This theorem is used by:  necomi  3011  necomd  3012  dfdif3  4069  0pss  4363  iftrueb  4498  disjtp2  4680  difprsn1  4766  difprsn2  4767  prproe  4868  fndmdifcom  7039  fvpr1g  7192  fvpr2g  7193  fvtp1  7197  fvtp2  7198  fvtp3  7199  fvtp1g  7200  fvtp2g  7201  fvtp3g  7202  dff14b  7272  f12dfv  7278  f13dfv  7279  orduniorsuc  7830  kmlem3  10159  kmlem4  10160  ac6num  10485  leltne  11327  nn0lt2  12688  xrleltne  13200  fzofzim  13769  elfznelfzo  13833  elfznelfzob  13834  fleqceilz  13919  hashdifpr  14484  hashgt12el  14491  hashgt12el2  14492  hashgt23el  14493  hash7g  14555  cshw0  14869  cshwn  14872  isprm2lem  16777  prm2orodd  16787  cshwsdisj  17196  sgrp2nmndlem5  19047  f1omvdconj  19579  pmtrprfv3  19587  pmtr3ncomlem1  19606  dmdprdd  20134  cnfldfunALT  21606  xrsdsreclblem  21632  xrsdsreclb  21633  ordthaus  23615  hmphindis  24029  angpined  27075  nosgnn0  27902  noextendlt  27913  nosepne  27924  nosepdm  27928  nosupbnd2lem1  27959  noinfbnd2lem1  27974  noetasuplem4  27980  funvtxval0  29480  snstrvtxval  29502  snstriedgval  29503  nbgrsym  29831  nb3grprlem2  29849  nb3grpr  29850  cusgredg  29892  cplgr3v  29903  1egrvtxdg0  29979  usgr2pthlem  30236  usgr2pth0  30238  2pthdlem1  30406  clwlkclwwlklem2a4  30475  uhgr3cyclex  30670  eupth2lem3lem4  30719  frcond1  30754  frcond4  30758  frgr3v  30763  3vfriswmgr  30766  2pthfrgr  30772  3cyclfrgrrn1  30773  n4cyclfrgr  30779  frgrnbnb  30781  frgrwopreglem4a  30798  ch0pss  31934  pmtrprfv2  33536  esumcvgre  34609  bnj563  35261  cusgredgex2  35729  cvmsdisj  35857  fmlaomn0  35977  ex-sategoelel  36008  btwnouttr  36612  fscgr  36668  linecom  36738  linerflx2  36739  mh-inf3f1  37168  poimirlem25  38402  divrngidl  38786  lcvbr3  39904  opltn0  40071  atlltn0  40187  2dim  40351  ps-2  40359  islln3  40391  llnexatN  40402  4atlem11  40490  isline4N  40658  lhpex2leN  40894  cdleme48gfv  41418  60gcd7e1  42879  dvrelogpow2b  42942  aks4d1p1p4  42945  aks6d1c2p2  42993  fsuppind  43444  onov0suclim  44123  oenassex  44167  pr2eldif2  44403  pimxrneun  46324  icccncfext  46723  fourierdlem42  46985  sqrtnzqaa  47740  icceuelpartlem  48343  ichnreuop  48380  paireqne  48419  oddprmALTV  48611  rrx2pnedifcoorneor  49654  rrx2linest  49680