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  4676  difprsn1  4762  difprsn2  4763  prproe  4864  fndmdifcom  7042  fvpr1g  7195  fvpr2g  7196  fvtp1  7200  fvtp2  7201  fvtp3  7202  fvtp1g  7203  fvtp2g  7204  fvtp3g  7205  dff14b  7275  f12dfv  7281  f13dfv  7282  orduniorsuc  7841  onelfvnef1  8449  kmlem3  10231  kmlem4  10232  ac6num  10557  leltne  11399  nn0lt2  12762  xrleltne  13274  fzofzim  13844  elfznelfzo  13908  elfznelfzob  13909  fleqceilz  13994  hashdifpr  14560  hashgt12el  14567  hashgt12el2  14568  hashgt23el  14569  hash7g  14631  cshw0  14945  cshwn  14948  isprm2lem  16856  prm2orodd  16866  cshwsdisj  17276  sgrp2nmndlem5  19128  f1omvdconj  19660  pmtrprfv3  19668  pmtr3ncomlem1  19687  dmdprdd  20215  cnfldfunALT  21693  xrsdsreclblem  21719  xrsdsreclb  21720  ordthaus  23702  hmphindis  24116  angpined  27158  nosgnn0  28015  noextendlt  28026  nosepne  28037  nosepdm  28041  nosupbnd2lem1  28072  noinfbnd2lem1  28087  noetasuplem4  28093  funvtxval0  29593  snstrvtxval  29615  snstriedgval  29616  nbgrsym  29944  nb3grprlem2  29962  nb3grpr  29963  cusgredg  30005  cplgr3v  30016  1egrvtxdg0  30092  usgr2pthlem  30349  usgr2pth0  30351  2pthdlem1  30519  clwlkclwwlklem2a4  30588  uhgr3cyclex  30783  eupth2lem3lem4  30832  frcond1  30867  frcond4  30871  frgr3v  30876  3vfriswmgr  30879  2pthfrgr  30885  3cyclfrgrrn1  30886  n4cyclfrgr  30892  frgrnbnb  30894  frgrwopreglem4a  30911  ch0pss  32047  pmtrprfv2  33649  esumcvgre  34723  bnj563  35374  cusgredgex2  35907  cvmsdisj  36035  fmlaomn0  36155  ex-sategoelel  36186  btwnouttr  36789  fscgr  36845  linecom  36915  linerflx2  36916  poimirlem25  38564  divrngidl  38963  lcvbr3  40081  opltn0  40248  atlltn0  40364  2dim  40528  ps-2  40536  islln3  40568  llnexatN  40579  4atlem11  40667  isline4N  40835  lhpex2leN  41071  cdleme48gfv  41595  60gcd7e1  43056  dvrelogpow2b  43119  aks4d1p1p4  43122  aks6d1c2p2  43170  fsuppind  43619  onov0suclim  44276  oenassex  44320  pr2eldif2  44556  pimxrneun  46498  icccncfext  46897  fourierdlem42  47159  sqrtnzqaa  47914  icceuelpartlem  48517  ichnreuop  48554  paireqne  48593  oddprmALTV  48785  rrx2pnedifcoorneor  49828  rrx2linest  49854