Theorem necom 3009

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 208   ≠ wne 2956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ne 2957

This theorem is referenced by:  necomi  3010  necomd  3011  dfdif3  4071  0pss  4400  iftrueb  4492  disjtp2  4674  difprsn1  4759  difprsn2  4760  prproe  4862  fndmdifcom  7020  fvpr1g  7170  fvpr2g  7171  fvtp1  7175  fvtp2  7176  fvtp3  7177  fvtp1g  7178  fvtp2g  7179  fvtp3g  7180  dff14b  7251  f12dfv  7253  f13dfv  7254  orduniorsuc  7806  kmlem3  10106  kmlem4  10107  ac6num  10433  leltne  11269  nn0lt2  12633  xrleltne  13144  fzofzim  13712  elfznelfzo  13776  elfznelfzob  13777  fleqceilz  13861  hashdifpr  14425  hashgt12el  14432  hashgt12el2  14433  hashgt23el  14434  hash7g  14496  cshw0  14804  cshwn  14807  isprm2lem  16698  prm2orodd  16708  cshwsdisj  17117  sgrp2nmndlem5  18949  f1omvdconj  19469  pmtrprfv3  19477  pmtr3ncomlem1  19496  dmdprdd  20024  cnfldfunALT  21419  xrsdsreclblem  21445  xrsdsreclb  21446  ordthaus  23424  hmphindis  23837  angpined  26872  nosgnn0  27699  noextendlt  27710  nosepne  27721  nosepdm  27725  nosupbnd2lem1  27756  noinfbnd2lem1  27771  noetasuplem4  27777  funvtxval0  29162  snstrvtxval  29184  snstriedgval  29185  nbgrsym  29510  nb3grprlem2  29528  nb3grpr  29529  cusgredg  29571  cplgr3v  29582  1egrvtxdg0  29658  usgr2pthlem  29909  usgr2pth0  29911  2pthdlem1  30076  clwlkclwwlklem2a4  30145  uhgr3cyclex  30330  eupth2lem3lem4  30379  frcond1  30414  frcond4  30418  frgr3v  30423  3vfriswmgr  30426  2pthfrgr  30432  3cyclfrgrrn1  30433  n4cyclfrgr  30439  frgrnbnb  30441  frgrwopreglem4a  30458  ch0pss  31594  pmtrprfv2  33229  esumcvgre  34349  bnj563  35003  cusgredgex2  35437  cvmsdisj  35584  fmlaomn0  35704  ex-sategoelel  35735  btwnouttr  36338  fscgr  36394  linecom  36464  linerflx2  36465  mh-inf3f1  36865  poimirlem25  38108  divrngidl  38491  lcvbr3  39611  opltn0  39778  atlltn0  39894  2dim  40058  ps-2  40066  islln3  40098  llnexatN  40109  4atlem11  40197  isline4N  40365  lhpex2leN  40601  cdleme48gfv  41125  60gcd7e1  42586  dvrelogpow2b  42649  aks4d1p1p4  42652  aks6d1c2p2  42700  fsuppind  43136  onov0suclim  43815  oenassex  43859  pr2eldif2  44095  pimxrneun  46026  icccncfext  46425  fourierdlem42  46687  icceuelpartlem  48005  ichnreuop  48042  paireqne  48081  oddprmALTV  48273  rrx2pnedifcoorneor  49302  rrx2linest  49328