Theorem necom 3011

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 3010	1 ⊢ (𝐴 ≠ 𝐵 ↔ 𝐵 ≠ 𝐴)

Syntax hints:   ↔ wb 209   ≠ wne 2958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ne 2959

This theorem is referenced by:  necomi  3012  necomd  3013  dfdif3  4073  0pss  4368  iftrueb  4501  disjtp2  4683  difprsn1  4769  difprsn2  4770  prproe  4871  fndmdifcom  7040  fvpr1g  7190  fvpr2g  7191  fvtp1  7195  fvtp2  7196  fvtp3  7197  fvtp1g  7198  fvtp2g  7199  fvtp3g  7200  dff14b  7271  f12dfv  7273  f13dfv  7274  orduniorsuc  7827  kmlem3  10137  kmlem4  10138  ac6num  10464  leltne  11300  nn0lt2  12660  xrleltne  13171  fzofzim  13740  elfznelfzo  13804  elfznelfzob  13805  fleqceilz  13889  hashdifpr  14454  hashgt12el  14461  hashgt12el2  14462  hashgt23el  14463  hash7g  14525  cshw0  14833  cshwn  14836  isprm2lem  16740  prm2orodd  16750  cshwsdisj  17159  sgrp2nmndlem5  18992  f1omvdconj  19517  pmtrprfv3  19525  pmtr3ncomlem1  19544  dmdprdd  20072  cnfldfunALT  21518  xrsdsreclblem  21544  xrsdsreclb  21545  ordthaus  23522  hmphindis  23935  angpined  26976  nosgnn0  27803  noextendlt  27814  nosepne  27825  nosepdm  27829  nosupbnd2lem1  27860  noinfbnd2lem1  27875  noetasuplem4  27881  funvtxval0  29346  snstrvtxval  29368  snstriedgval  29369  nbgrsym  29694  nb3grprlem2  29712  nb3grpr  29713  cusgredg  29755  cplgr3v  29766  1egrvtxdg0  29842  usgr2pthlem  30093  usgr2pth0  30095  2pthdlem1  30260  clwlkclwwlklem2a4  30329  uhgr3cyclex  30514  eupth2lem3lem4  30563  frcond1  30598  frcond4  30602  frgr3v  30607  3vfriswmgr  30610  2pthfrgr  30616  3cyclfrgrrn1  30617  n4cyclfrgr  30623  frgrnbnb  30625  frgrwopreglem4a  30642  ch0pss  31778  pmtrprfv2  33389  esumcvgre  34462  bnj563  35113  cusgredgex2  35596  cvmsdisj  35743  fmlaomn0  35863  ex-sategoelel  35894  btwnouttr  36497  fscgr  36553  linecom  36623  linerflx2  36624  mh-inf3f1  37033  poimirlem25  38277  divrngidl  38660  lcvbr3  39778  opltn0  39945  atlltn0  40061  2dim  40225  ps-2  40233  islln3  40265  llnexatN  40276  4atlem11  40364  isline4N  40532  lhpex2leN  40768  cdleme48gfv  41292  60gcd7e1  42753  dvrelogpow2b  42816  aks4d1p1p4  42819  aks6d1c2p2  42867  fsuppind  43305  onov0suclim  43984  oenassex  44028  pr2eldif2  44264  pimxrneun  46185  icccncfext  46584  fourierdlem42  46846  sqrtnzqaa  47588  icceuelpartlem  48167  ichnreuop  48204  paireqne  48243  oddprmALTV  48435  rrx2pnedifcoorneor  49479  rrx2linest  49505