Theorem necom 2988

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

Syntax hints:   ↔ wb 207   ≠ wne 2935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ne 2936

This theorem is referenced by:  necomi  2989  necomd  2990  dfdif3  4055  0pss  4382  iftrueb  4474  disjtp2  4655  difprsn1  4740  difprsn2  4741  prproe  4843  fndmdifcom  6991  fvpr1g  7141  fvpr2g  7142  fvtp1  7146  fvtp2  7147  fvtp3  7148  fvtp1g  7149  fvtp2g  7150  fvtp3g  7151  dff14b  7222  f12dfv  7224  f13dfv  7225  orduniorsuc  7777  kmlem3  10073  kmlem4  10074  ac6num  10399  leltne  11233  nn0lt2  12590  xrleltne  13094  fzofzim  13662  elfznelfzo  13726  elfznelfzob  13727  fleqceilz  13811  hashdifpr  14375  hashgt12el  14382  hashgt12el2  14383  hashgt23el  14384  hash7g  14446  cshw0  14754  cshwn  14757  isprm2lem  16648  prm2orodd  16658  cshwsdisj  17067  sgrp2nmndlem5  18898  f1omvdconj  19419  pmtrprfv3  19427  pmtr3ncomlem1  19446  dmdprdd  19974  cnfldfunALT  21369  xrsdsreclblem  21395  xrsdsreclb  21396  ordthaus  23374  hmphindis  23787  angpined  26819  nosgnn0  27647  noextendlt  27658  nosepne  27669  nosepdm  27673  nosupbnd2lem1  27704  noinfbnd2lem1  27719  noetasuplem4  27725  funvtxval0  29109  snstrvtxval  29131  snstriedgval  29132  nbgrsym  29457  nb3grprlem2  29475  nb3grpr  29476  cusgredg  29518  cplgr3v  29529  1egrvtxdg0  29605  usgr2pthlem  29856  usgr2pth0  29858  2pthdlem1  30023  clwlkclwwlklem2a4  30092  uhgr3cyclex  30277  eupth2lem3lem4  30326  frcond1  30361  frcond4  30365  frgr3v  30370  3vfriswmgr  30373  2pthfrgr  30379  3cyclfrgrrn1  30380  n4cyclfrgr  30386  frgrnbnb  30388  frgrwopreglem4a  30405  ch0pss  31541  pmtrprfv2  33176  esumcvgre  34282  bnj563  34933  cusgredgex2  35358  cvmsdisj  35505  fmlaomn0  35625  ex-sategoelel  35656  btwnouttr  36259  fscgr  36315  linecom  36385  linerflx2  36386  mh-inf3f1  36776  poimirlem25  38019  divrngidl  38402  lcvbr3  39522  opltn0  39689  atlltn0  39805  2dim  39969  ps-2  39977  islln3  40009  llnexatN  40020  4atlem11  40108  isline4N  40276  lhpex2leN  40512  cdleme48gfv  41036  60gcd7e1  42497  dvrelogpow2b  42560  aks4d1p1p4  42563  aks6d1c2p2  42611  fsuppind  43047  onov0suclim  43726  oenassex  43770  pr2eldif2  44006  pimxrneun  45938  icccncfext  46337  fourierdlem42  46599  icceuelpartlem  47917  ichnreuop  47954  paireqne  47993  oddprmALTV  48185  rrx2pnedifcoorneor  49214  rrx2linest  49240