Theorem necom 2978

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 206   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  necomi  2979  necomd  2980  dfdif3  4070  0pss  4400  iftrueb  4491  disjtp2  4670  difprsn1  4754  difprsn2  4755  prproe  4859  fndmdifcom  6981  fvpr1g  7130  fvpr2g  7131  fvtp1  7135  fvtp2  7136  fvtp3  7137  fvtp1g  7138  fvtp2g  7139  fvtp3g  7140  dff14b  7212  f12dfv  7214  f13dfv  7215  orduniorsuc  7769  kmlem3  10066  kmlem4  10067  ac6num  10392  leltne  11223  nn0lt2  12557  xrleltne  13065  fzofzim  13630  elfznelfzo  13693  elfznelfzob  13694  fleqceilz  13776  hashdifpr  14340  hashgt12el  14347  hashgt12el2  14348  hashgt23el  14349  hash7g  14411  cshw0  14718  cshwn  14721  isprm2lem  16610  prm2orodd  16620  cshwsdisj  17028  sgrp2nmndlem5  18821  f1omvdconj  19343  pmtrprfv3  19351  pmtr3ncomlem1  19370  dmdprdd  19898  cnfldfunALT  21294  cnfldfunALTOLD  21307  xrsdsreclblem  21337  xrsdsreclb  21338  ordthaus  23287  hmphindis  23700  angpined  26756  nosgnn0  27586  noextendlt  27597  nosepne  27608  nosepdm  27612  nosupbnd2lem1  27643  noinfbnd2lem1  27658  noetasuplem4  27664  funvtxval0  28978  snstrvtxval  29000  snstriedgval  29001  nbgrsym  29326  nb3grprlem2  29344  nb3grpr  29345  cusgredg  29387  cplgr3v  29398  1egrvtxdg0  29475  usgr2pthlem  29726  usgr2pth0  29728  2pthdlem1  29893  clwlkclwwlklem2a4  29959  uhgr3cyclex  30144  eupth2lem3lem4  30193  frcond1  30228  frcond4  30232  frgr3v  30237  3vfriswmgr  30240  2pthfrgr  30246  3cyclfrgrrn1  30247  n4cyclfrgr  30253  frgrnbnb  30255  frgrwopreglem4a  30272  ch0pss  31407  pmtrprfv2  33043  esumcvgre  34060  bnj563  34712  cusgredgex2  35098  cvmsdisj  35245  fmlaomn0  35365  ex-sategoelel  35396  btwnouttr  36000  fscgr  36056  linecom  36126  linerflx2  36127  poimirlem25  37627  divrngidl  38010  lcvbr3  39004  opltn0  39171  atlltn0  39287  2dim  39452  ps-2  39460  islln3  39492  llnexatN  39503  4atlem11  39591  isline4N  39759  lhpex2leN  39995  cdleme48gfv  40519  60gcd7e1  41981  dvrelogpow2b  42044  aks4d1p1p4  42047  aks6d1c2p2  42095  fsuppind  42566  onov0suclim  43250  oenassex  43294  pr2eldif2  43531  pimxrneun  45471  icccncfext  45872  fourierdlem42  46134  icceuelpartlem  47423  ichnreuop  47460  paireqne  47499  oddprmALTV  47675  rrx2pnedifcoorneor  48705  rrx2linest  48731