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  4080  0pss  4410  iftrueb  4501  disjtp2  4680  difprsn1  4764  difprsn2  4765  prproe  4869  fndmdifcom  7015  fvpr1g  7164  fvpr2g  7165  fvtp1  7169  fvtp2  7170  fvtp3  7171  fvtp1g  7172  fvtp2g  7173  fvtp3g  7174  dff14b  7246  f12dfv  7248  f13dfv  7249  orduniorsuc  7805  kmlem3  10106  kmlem4  10107  ac6num  10432  leltne  11263  nn0lt2  12597  xrleltne  13105  fzofzim  13670  elfznelfzo  13733  elfznelfzob  13734  fleqceilz  13816  hashdifpr  14380  hashgt12el  14387  hashgt12el2  14388  hashgt23el  14389  hash7g  14451  cshw0  14759  cshwn  14762  isprm2lem  16651  prm2orodd  16661  cshwsdisj  17069  sgrp2nmndlem5  18856  f1omvdconj  19376  pmtrprfv3  19384  pmtr3ncomlem1  19403  dmdprdd  19931  cnfldfunALT  21279  cnfldfunALTOLD  21292  xrsdsreclblem  21329  xrsdsreclb  21330  ordthaus  23271  hmphindis  23684  angpined  26740  nosgnn0  27570  noextendlt  27581  nosepne  27592  nosepdm  27596  nosupbnd2lem1  27627  noinfbnd2lem1  27642  noetasuplem4  27648  funvtxval0  28942  snstrvtxval  28964  snstriedgval  28965  nbgrsym  29290  nb3grprlem2  29308  nb3grpr  29309  cusgredg  29351  cplgr3v  29362  1egrvtxdg0  29439  usgr2pthlem  29693  usgr2pth0  29695  2pthdlem1  29860  clwlkclwwlklem2a4  29926  uhgr3cyclex  30111  eupth2lem3lem4  30160  frcond1  30195  frcond4  30199  frgr3v  30204  3vfriswmgr  30207  2pthfrgr  30213  3cyclfrgrrn1  30214  n4cyclfrgr  30220  frgrnbnb  30222  frgrwopreglem4a  30239  ch0pss  31374  pmtrprfv2  33045  esumcvgre  34081  bnj563  34733  cusgredgex2  35110  cvmsdisj  35257  fmlaomn0  35377  ex-sategoelel  35408  btwnouttr  36012  fscgr  36068  linecom  36138  linerflx2  36139  poimirlem25  37639  divrngidl  38022  lcvbr3  39016  opltn0  39183  atlltn0  39299  2dim  39464  ps-2  39472  islln3  39504  llnexatN  39515  4atlem11  39603  isline4N  39771  lhpex2leN  40007  cdleme48gfv  40531  60gcd7e1  41993  dvrelogpow2b  42056  aks4d1p1p4  42059  aks6d1c2p2  42107  fsuppind  42578  onov0suclim  43263  oenassex  43307  pr2eldif2  43544  pimxrneun  45484  icccncfext  45885  fourierdlem42  46147  icceuelpartlem  47436  ichnreuop  47473  paireqne  47512  oddprmALTV  47688  rrx2pnedifcoorneor  48705  rrx2linest  48731