Theorem necom 3000

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 206   ≠ wne 2946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ne 2947

This theorem is referenced by:  necomi  3001  necomd  3002  dfdif3  4140  0pss  4470  disjtp2  4741  difprsn1  4825  difprsn2  4826  prproe  4929  fndmdifcom  7076  fvpr1g  7224  fvpr2g  7225  fvpr1OLD  7228  fvpr2OLD  7230  fvtp1  7232  fvtp2  7233  fvtp3  7234  fvtp1g  7235  fvtp2g  7236  fvtp3g  7237  dff14b  7308  f12dfv  7309  f13dfv  7310  orduniorsuc  7866  kmlem3  10222  kmlem4  10223  ac6num  10548  leltne  11379  nn0lt2  12706  xrleltne  13207  fzofzim  13763  elfznelfzo  13822  elfznelfzob  13823  fleqceilz  13905  hashdifpr  14464  hashgt12el  14471  hashgt12el2  14472  hashgt23el  14473  hash7g  14535  cshw0  14842  cshwn  14845  isprm2lem  16728  prm2orodd  16738  cshwsdisj  17146  sgrp2nmndlem5  18964  f1omvdconj  19488  pmtrprfv3  19496  pmtr3ncomlem1  19515  dmdprdd  20043  cnfldfunALT  21402  cnfldfunALTOLD  21415  xrsdsreclblem  21453  xrsdsreclb  21454  ordthaus  23413  hmphindis  23826  angpined  26891  nosgnn0  27721  noextendlt  27732  nosepne  27743  nosepdm  27747  nosupbnd2lem1  27778  noinfbnd2lem1  27793  noetasuplem4  27799  funvtxval0  29050  snstrvtxval  29072  snstriedgval  29073  nbgrsym  29398  nb3grprlem2  29416  nb3grpr  29417  cusgredg  29459  cplgr3v  29470  1egrvtxdg0  29547  usgr2pthlem  29799  usgr2pth0  29801  2pthdlem1  29963  clwlkclwwlklem2a4  30029  uhgr3cyclex  30214  eupth2lem3lem4  30263  frcond1  30298  frcond4  30302  frgr3v  30307  3vfriswmgr  30310  2pthfrgr  30316  3cyclfrgrrn1  30317  n4cyclfrgr  30323  frgrnbnb  30325  frgrwopreglem4a  30342  ch0pss  31477  pmtrprfv2  33081  esumcvgre  34055  bnj563  34719  cusgredgex2  35090  cvmsdisj  35238  fmlaomn0  35358  ex-sategoelel  35389  btwnouttr  35988  fscgr  36044  linecom  36114  linerflx2  36115  poimirlem25  37605  divrngidl  37988  lcvbr3  38979  opltn0  39146  atlltn0  39262  2dim  39427  ps-2  39435  islln3  39467  llnexatN  39478  4atlem11  39566  isline4N  39734  lhpex2leN  39970  cdleme48gfv  40494  60gcd7e1  41962  dvrelogpow2b  42025  aks4d1p1p4  42028  aks6d1c2p2  42076  fsuppind  42545  onov0suclim  43236  oenassex  43280  pr2eldif2  43517  pimxrneun  45404  icccncfext  45808  fourierdlem42  46070  icceuelpartlem  47309  ichnreuop  47346  paireqne  47385  oddprmALTV  47561  rrx2pnedifcoorneor  48450  rrx2linest  48476