Theorem necom 2986

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 206   ≠ wne 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934

This theorem is referenced by:  necomi  2987  necomd  2988  dfdif3  4058  0pss  4388  iftrueb  4480  disjtp2  4661  difprsn1  4744  difprsn2  4745  prproe  4849  fndmdifcom  6989  fvpr1g  7138  fvpr2g  7139  fvtp1  7143  fvtp2  7144  fvtp3  7145  fvtp1g  7146  fvtp2g  7147  fvtp3g  7148  dff14b  7219  f12dfv  7221  f13dfv  7222  orduniorsuc  7774  kmlem3  10066  kmlem4  10067  ac6num  10392  leltne  11226  nn0lt2  12583  xrleltne  13087  fzofzim  13655  elfznelfzo  13719  elfznelfzob  13720  fleqceilz  13804  hashdifpr  14368  hashgt12el  14375  hashgt12el2  14376  hashgt23el  14377  hash7g  14439  cshw0  14747  cshwn  14750  isprm2lem  16641  prm2orodd  16651  cshwsdisj  17060  sgrp2nmndlem5  18891  f1omvdconj  19412  pmtrprfv3  19420  pmtr3ncomlem1  19439  dmdprdd  19967  cnfldfunALT  21359  cnfldfunALTOLD  21372  xrsdsreclblem  21402  xrsdsreclb  21403  ordthaus  23359  hmphindis  23772  angpined  26807  nosgnn0  27636  noextendlt  27647  nosepne  27658  nosepdm  27662  nosupbnd2lem1  27693  noinfbnd2lem1  27708  noetasuplem4  27714  funvtxval0  29098  snstrvtxval  29120  snstriedgval  29121  nbgrsym  29446  nb3grprlem2  29464  nb3grpr  29465  cusgredg  29507  cplgr3v  29518  1egrvtxdg0  29595  usgr2pthlem  29846  usgr2pth0  29848  2pthdlem1  30013  clwlkclwwlklem2a4  30082  uhgr3cyclex  30267  eupth2lem3lem4  30316  frcond1  30351  frcond4  30355  frgr3v  30360  3vfriswmgr  30363  2pthfrgr  30369  3cyclfrgrrn1  30370  n4cyclfrgr  30376  frgrnbnb  30378  frgrwopreglem4a  30395  ch0pss  31531  pmtrprfv2  33164  esumcvgre  34251  bnj563  34902  cusgredgex2  35321  cvmsdisj  35468  fmlaomn0  35588  ex-sategoelel  35619  btwnouttr  36222  fscgr  36278  linecom  36348  linerflx2  36349  mh-inf3f1  36739  poimirlem25  37980  divrngidl  38363  lcvbr3  39483  opltn0  39650  atlltn0  39766  2dim  39930  ps-2  39938  islln3  39970  llnexatN  39981  4atlem11  40069  isline4N  40237  lhpex2leN  40473  cdleme48gfv  40997  60gcd7e1  42458  dvrelogpow2b  42521  aks4d1p1p4  42524  aks6d1c2p2  42572  fsuppind  43037  onov0suclim  43720  oenassex  43764  pr2eldif2  44000  pimxrneun  45934  icccncfext  46333  fourierdlem42  46595  icceuelpartlem  47907  ichnreuop  47944  paireqne  47983  oddprmALTV  48175  rrx2pnedifcoorneor  49204  rrx2linest  49230