Theorem necom 3009

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

Assertion

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

Proof of Theorem necom

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

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

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 2733

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

This theorem is used by:  necomi  3010  necomd  3011  dfdif3  4066  0pss  4360  iftrueb  4495  disjtp2  4677  difprsn1  4763  difprsn2  4764  prproe  4865  fndmdifcom  7034  fvpr1g  7187  fvpr2g  7188  fvtp1  7192  fvtp2  7193  fvtp3  7194  fvtp1g  7195  fvtp2g  7196  fvtp3g  7197  dff14b  7267  f12dfv  7273  f13dfv  7274  orduniorsuc  7830  onelfvnef1  8433  kmlem3  10212  kmlem4  10213  ac6num  10538  leltne  11380  nn0lt2  12743  xrleltne  13255  fzofzim  13824  elfznelfzo  13888  elfznelfzob  13889  fleqceilz  13974  hashdifpr  14540  hashgt12el  14547  hashgt12el2  14548  hashgt23el  14549  hash7g  14611  cshw0  14925  cshwn  14928  isprm2lem  16836  prm2orodd  16846  cshwsdisj  17256  sgrp2nmndlem5  19108  f1omvdconj  19640  pmtrprfv3  19648  pmtr3ncomlem1  19667  dmdprdd  20195  cnfldfunALT  21673  xrsdsreclblem  21699  xrsdsreclb  21700  ordthaus  23682  hmphindis  24096  angpined  27140  nosgnn0  27997  noextendlt  28008  nosepne  28019  nosepdm  28023  nosupbnd2lem1  28054  noinfbnd2lem1  28069  noetasuplem4  28075  funvtxval0  29575  snstrvtxval  29597  snstriedgval  29598  nbgrsym  29926  nb3grprlem2  29944  nb3grpr  29945  cusgredg  29987  cplgr3v  29998  1egrvtxdg0  30074  usgr2pthlem  30331  usgr2pth0  30333  2pthdlem1  30501  clwlkclwwlklem2a4  30570  uhgr3cyclex  30765  eupth2lem3lem4  30814  frcond1  30849  frcond4  30853  frgr3v  30858  3vfriswmgr  30861  2pthfrgr  30867  3cyclfrgrrn1  30868  n4cyclfrgr  30874  frgrnbnb  30876  frgrwopreglem4a  30893  ch0pss  32029  pmtrprfv2  33631  esumcvgre  34705  bnj563  35357  cusgredgex2  35876  cvmsdisj  36004  fmlaomn0  36124  ex-sategoelel  36155  btwnouttr  36759  fscgr  36815  linecom  36885  linerflx2  36886  poimirlem25  38531  divrngidl  38930  lcvbr3  40048  opltn0  40215  atlltn0  40331  2dim  40495  ps-2  40503  islln3  40535  llnexatN  40546  4atlem11  40634  isline4N  40802  lhpex2leN  41038  cdleme48gfv  41562  60gcd7e1  43023  dvrelogpow2b  43086  aks4d1p1p4  43089  aks6d1c2p2  43137  fsuppind  43580  onov0suclim  44234  oenassex  44278  pr2eldif2  44514  pimxrneun  46442  icccncfext  46841  fourierdlem42  47103  sqrtnzqaa  47858  icceuelpartlem  48461  ichnreuop  48498  paireqne  48537  oddprmALTV  48729  rrx2pnedifcoorneor  49772  rrx2linest  49798