Theorem necom 2996

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 205   ≠ wne 2942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-ne 2943

This theorem is referenced by:  necomi  2997  necomd  2998  0pss  4375  disjtp2  4649  difprsn1  4730  difprsn2  4731  prproe  4834  fndmdifcom  6902  fvpr1g  7044  fvpr2g  7045  fvpr1OLD  7048  fvpr2OLD  7050  fvtp1  7052  fvtp2  7053  fvtp3  7054  fvtp1g  7055  fvtp2g  7056  fvtp3g  7057  dff14b  7125  f12dfv  7126  f13dfv  7127  orduniorsuc  7652  kmlem3  9839  kmlem4  9840  ac6num  10166  leltne  10995  nn0lt2  12313  xrleltne  12808  fzofzim  13362  elfznelfzo  13420  elfznelfzob  13421  fleqceilz  13502  hashdifpr  14058  hashgt12el  14065  hashgt12el2  14066  hashgt23el  14067  cshw0  14435  cshwn  14438  isprm2lem  16314  prm2orodd  16324  cshwsdisj  16728  sgrp2nmndlem5  18483  f1omvdconj  18969  pmtrprfv3  18977  pmtr3ncomlem1  18996  dmdprdd  19517  xrsdsreclblem  20556  xrsdsreclb  20557  ordthaus  22443  hmphindis  22856  angpined  25885  funvtxval0  27288  snstrvtxval  27310  snstriedgval  27311  nbgrsym  27633  nb3grprlem2  27651  nb3grpr  27652  cusgredg  27694  cplgr3v  27705  1egrvtxdg0  27781  usgr2pthlem  28032  usgr2pth0  28034  2pthdlem1  28196  clwlkclwwlklem2a4  28262  uhgr3cyclex  28447  eupth2lem3lem4  28496  frcond1  28531  frcond4  28535  frgr3v  28540  3vfriswmgr  28543  2pthfrgr  28549  3cyclfrgrrn1  28550  n4cyclfrgr  28556  frgrnbnb  28558  frgrwopreglem4a  28575  ch0pss  29708  pmtrprfv2  31259  esumcvgre  31959  bnj563  32623  cusgredgex2  32984  cvmsdisj  33132  fmlaomn0  33252  ex-sategoelel  33283  nosgnn0  33788  noextendlt  33799  nosepne  33810  nosepdm  33814  nosupbnd2lem1  33845  noinfbnd2lem1  33860  noetasuplem4  33866  btwnouttr  34253  fscgr  34309  linecom  34379  linerflx2  34380  poimirlem25  35729  divrngidl  36113  lcvbr3  36964  opltn0  37131  atlltn0  37247  2dim  37411  ps-2  37419  islln3  37451  llnexatN  37462  4atlem11  37550  isline4N  37718  lhpex2leN  37954  cdleme48gfv  38478  60gcd7e1  39941  dvrelogpow2b  40004  aks4d1p1p4  40007  fsuppind  40202  pr2eldif2  41051  icccncfext  43318  fourierdlem42  43580  icceuelpartlem  44775  ichnreuop  44812  paireqne  44851  oddprmALTV  45027  rrx2pnedifcoorneor  45950  rrx2linest  45976