Theorem necom 2982

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 206   ≠ wne 2929

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 2705

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

This theorem is referenced by:  necomi  2983  necomd  2984  dfdif3  4066  0pss  4396  iftrueb  4487  disjtp2  4668  difprsn1  4751  difprsn2  4752  prproe  4856  fndmdifcom  6982  fvpr1g  7130  fvpr2g  7131  fvtp1  7135  fvtp2  7136  fvtp3  7137  fvtp1g  7138  fvtp2g  7139  fvtp3g  7140  dff14b  7211  f12dfv  7213  f13dfv  7214  orduniorsuc  7766  kmlem3  10051  kmlem4  10052  ac6num  10377  leltne  11209  nn0lt2  12542  xrleltne  13046  fzofzim  13611  elfznelfzo  13675  elfznelfzob  13676  fleqceilz  13760  hashdifpr  14324  hashgt12el  14331  hashgt12el2  14332  hashgt23el  14333  hash7g  14395  cshw0  14703  cshwn  14706  isprm2lem  16594  prm2orodd  16604  cshwsdisj  17012  sgrp2nmndlem5  18839  f1omvdconj  19360  pmtrprfv3  19368  pmtr3ncomlem1  19387  dmdprdd  19915  cnfldfunALT  21308  cnfldfunALTOLD  21321  xrsdsreclblem  21351  xrsdsreclb  21352  ordthaus  23300  hmphindis  23713  angpined  26768  nosgnn0  27598  noextendlt  27609  nosepne  27620  nosepdm  27624  nosupbnd2lem1  27655  noinfbnd2lem1  27670  noetasuplem4  27676  funvtxval0  28995  snstrvtxval  29017  snstriedgval  29018  nbgrsym  29343  nb3grprlem2  29361  nb3grpr  29362  cusgredg  29404  cplgr3v  29415  1egrvtxdg0  29492  usgr2pthlem  29743  usgr2pth0  29745  2pthdlem1  29910  clwlkclwwlklem2a4  29979  uhgr3cyclex  30164  eupth2lem3lem4  30213  frcond1  30248  frcond4  30252  frgr3v  30257  3vfriswmgr  30260  2pthfrgr  30266  3cyclfrgrrn1  30267  n4cyclfrgr  30273  frgrnbnb  30275  frgrwopreglem4a  30292  ch0pss  31427  pmtrprfv2  33064  esumcvgre  34125  bnj563  34776  cusgredgex2  35188  cvmsdisj  35335  fmlaomn0  35455  ex-sategoelel  35486  btwnouttr  36089  fscgr  36145  linecom  36215  linerflx2  36216  poimirlem25  37706  divrngidl  38089  lcvbr3  39143  opltn0  39310  atlltn0  39426  2dim  39590  ps-2  39598  islln3  39630  llnexatN  39641  4atlem11  39729  isline4N  39897  lhpex2leN  40133  cdleme48gfv  40657  60gcd7e1  42119  dvrelogpow2b  42182  aks4d1p1p4  42185  aks6d1c2p2  42233  fsuppind  42709  onov0suclim  43392  oenassex  43436  pr2eldif2  43673  pimxrneun  45611  icccncfext  46010  fourierdlem42  46272  icceuelpartlem  47560  ichnreuop  47597  paireqne  47636  oddprmALTV  47812  rrx2pnedifcoorneor  48842  rrx2linest  48868