Theorem necom 3012

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

Assertion

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

Proof of Theorem necom

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  necomi  3013  necomd  3014  dfdif3  4058  0pss  4363  iftrueb  4498  disjtp2  4677  difprsn1  4763  difprsn2  4764  prproe  4836  fndmdifcom  7068  fvpr1g  7221  fvpr2g  7222  fvtp1  7226  fvtp2  7227  fvtp3  7228  fvtp1g  7229  fvtp2g  7230  fvtp3g  7231  dff14b  7301  f12dfv  7307  f13dfv  7308  orduniorsuc  7868  onelfvnef1  8480  kmlem3  10261  kmlem4  10262  ac6num  10587  leltne  11429  nn0lt2  12792  xrleltne  13304  fzofzim  13874  elfznelfzo  13938  elfznelfzob  13939  fleqceilz  14024  hashdifpr  14590  hashgt12el  14597  hashgt12el2  14598  hashgt23el  14599  hash7g  14661  cshw0  14976  cshwn  14979  isprm2lem  16888  prm2orodd  16898  cshwsdisj  17308  sgrp2nmndlem5  19160  f1omvdconj  19693  pmtrprfv3  19701  pmtr3ncomlem1  19720  dmdprdd  20248  cnfldfunALT  21726  xrsdsreclblem  21752  xrsdsreclb  21753  ordthaus  23735  hmphindis  24149  angpined  27191  nosgnn0  28048  noextendlt  28059  nosepne  28070  nosepdm  28074  nosupbnd2lem1  28105  noinfbnd2lem1  28120  noetasuplem4  28126  funvtxval0  29626  snstrvtxval  29648  snstriedgval  29649  nbgrsym  29977  nb3grprlem2  29995  nb3grpr  29996  cusgredg  30038  cplgr3v  30049  1egrvtxdg0  30125  usgr2pthlem  30382  usgr2pth0  30384  2pthdlem1  30552  clwlkclwwlklem2a4  30621  uhgr3cyclex  30816  eupth2lem3lem4  30865  frcond1  30900  frcond4  30904  frgr3v  30909  3vfriswmgr  30912  2pthfrgr  30918  3cyclfrgrrn1  30919  n4cyclfrgr  30925  frgrnbnb  30927  frgrwopreglem4a  30944  ch0pss  32080  pmtrprfv2  33725  esumcvgre  34806  bnj563  35457  cusgredgex2  36077  cvmsdisj  36215  fmlaomn0  36335  ex-sategoelel  36366  btwnouttr  36980  fscgr  37036  linecom  37106  linerflx2  37107  poimirlem25  38768  divrngidl  39165  lcvbr3  40283  opltn0  40450  atlltn0  40566  2dim  40730  ps-2  40738  islln3  40770  llnexatN  40781  4atlem11  40869  isline4N  41037  lhpex2leN  41273  cdleme48gfv  41797  60gcd7e1  43258  dvrelogpow2b  43321  aks4d1p1p4  43324  aks6d1c2p2  43372  fsuppind  43822  onov0suclim  44479  oenassex  44523  pr2eldif2  44759  pimxrneun  46713  icccncfext  47112  fourierdlem42  47374  sqrtnzqaa  48129  icceuelpartlem  48732  ichnreuop  48769  paireqne  48808  oddprmALTV  49000  rrx2pnedifcoorneor  50044  rrx2linest  50069