Theorem necom 2985

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 206   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ne 2933

This theorem is referenced by:  necomi  2986  necomd  2987  dfdif3  4069  0pss  4399  iftrueb  4492  disjtp2  4673  difprsn1  4756  difprsn2  4757  prproe  4861  fndmdifcom  6988  fvpr1g  7136  fvpr2g  7137  fvtp1  7141  fvtp2  7142  fvtp3  7143  fvtp1g  7144  fvtp2g  7145  fvtp3g  7146  dff14b  7217  f12dfv  7219  f13dfv  7220  orduniorsuc  7772  kmlem3  10063  kmlem4  10064  ac6num  10389  leltne  11222  nn0lt2  12555  xrleltne  13059  fzofzim  13625  elfznelfzo  13689  elfznelfzob  13690  fleqceilz  13774  hashdifpr  14338  hashgt12el  14345  hashgt12el2  14346  hashgt23el  14347  hash7g  14409  cshw0  14717  cshwn  14720  isprm2lem  16608  prm2orodd  16618  cshwsdisj  17026  sgrp2nmndlem5  18854  f1omvdconj  19375  pmtrprfv3  19383  pmtr3ncomlem1  19402  dmdprdd  19930  cnfldfunALT  21324  cnfldfunALTOLD  21337  xrsdsreclblem  21367  xrsdsreclb  21368  ordthaus  23328  hmphindis  23741  angpined  26796  nosgnn0  27626  noextendlt  27637  nosepne  27648  nosepdm  27652  nosupbnd2lem1  27683  noinfbnd2lem1  27698  noetasuplem4  27704  funvtxval0  29088  snstrvtxval  29110  snstriedgval  29111  nbgrsym  29436  nb3grprlem2  29454  nb3grpr  29455  cusgredg  29497  cplgr3v  29508  1egrvtxdg0  29585  usgr2pthlem  29836  usgr2pth0  29838  2pthdlem1  30003  clwlkclwwlklem2a4  30072  uhgr3cyclex  30257  eupth2lem3lem4  30306  frcond1  30341  frcond4  30345  frgr3v  30350  3vfriswmgr  30353  2pthfrgr  30359  3cyclfrgrrn1  30360  n4cyclfrgr  30366  frgrnbnb  30368  frgrwopreglem4a  30385  ch0pss  31520  pmtrprfv2  33170  esumcvgre  34248  bnj563  34899  cusgredgex2  35317  cvmsdisj  35464  fmlaomn0  35584  ex-sategoelel  35615  btwnouttr  36218  fscgr  36274  linecom  36344  linerflx2  36345  poimirlem25  37846  divrngidl  38229  lcvbr3  39283  opltn0  39450  atlltn0  39566  2dim  39730  ps-2  39738  islln3  39770  llnexatN  39781  4atlem11  39869  isline4N  40037  lhpex2leN  40273  cdleme48gfv  40797  60gcd7e1  42259  dvrelogpow2b  42322  aks4d1p1p4  42325  aks6d1c2p2  42373  fsuppind  42833  onov0suclim  43516  oenassex  43560  pr2eldif2  43796  pimxrneun  45732  icccncfext  46131  fourierdlem42  46393  icceuelpartlem  47681  ichnreuop  47718  paireqne  47757  oddprmALTV  47933  rrx2pnedifcoorneor  48962  rrx2linest  48988