Theorem necom 2994

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

Assertion

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

Proof of Theorem necom

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

Syntax hints:   ↔ wb 206   ≠ wne 2940

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 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ne 2941

This theorem is referenced by:  necomi  2995  necomd  2996  dfdif3  4117  0pss  4447  iftrueb  4538  disjtp2  4716  difprsn1  4800  difprsn2  4801  prproe  4905  fndmdifcom  7063  fvpr1g  7210  fvpr2g  7211  fvtp1  7215  fvtp2  7216  fvtp3  7217  fvtp1g  7218  fvtp2g  7219  fvtp3g  7220  dff14b  7291  f12dfv  7293  f13dfv  7294  orduniorsuc  7850  kmlem3  10193  kmlem4  10194  ac6num  10519  leltne  11350  nn0lt2  12681  xrleltne  13187  fzofzim  13749  elfznelfzo  13811  elfznelfzob  13812  fleqceilz  13894  hashdifpr  14454  hashgt12el  14461  hashgt12el2  14462  hashgt23el  14463  hash7g  14525  cshw0  14832  cshwn  14835  isprm2lem  16718  prm2orodd  16728  cshwsdisj  17136  sgrp2nmndlem5  18942  f1omvdconj  19464  pmtrprfv3  19472  pmtr3ncomlem1  19491  dmdprdd  20019  cnfldfunALT  21379  cnfldfunALTOLD  21392  xrsdsreclblem  21430  xrsdsreclb  21431  ordthaus  23392  hmphindis  23805  angpined  26873  nosgnn0  27703  noextendlt  27714  nosepne  27725  nosepdm  27729  nosupbnd2lem1  27760  noinfbnd2lem1  27775  noetasuplem4  27781  funvtxval0  29032  snstrvtxval  29054  snstriedgval  29055  nbgrsym  29380  nb3grprlem2  29398  nb3grpr  29399  cusgredg  29441  cplgr3v  29452  1egrvtxdg0  29529  usgr2pthlem  29783  usgr2pth0  29785  2pthdlem1  29950  clwlkclwwlklem2a4  30016  uhgr3cyclex  30201  eupth2lem3lem4  30250  frcond1  30285  frcond4  30289  frgr3v  30294  3vfriswmgr  30297  2pthfrgr  30303  3cyclfrgrrn1  30304  n4cyclfrgr  30310  frgrnbnb  30312  frgrwopreglem4a  30329  ch0pss  31464  pmtrprfv2  33108  esumcvgre  34092  bnj563  34757  cusgredgex2  35128  cvmsdisj  35275  fmlaomn0  35395  ex-sategoelel  35426  btwnouttr  36025  fscgr  36081  linecom  36151  linerflx2  36152  poimirlem25  37652  divrngidl  38035  lcvbr3  39024  opltn0  39191  atlltn0  39307  2dim  39472  ps-2  39480  islln3  39512  llnexatN  39523  4atlem11  39611  isline4N  39779  lhpex2leN  40015  cdleme48gfv  40539  60gcd7e1  42006  dvrelogpow2b  42069  aks4d1p1p4  42072  aks6d1c2p2  42120  fsuppind  42600  onov0suclim  43287  oenassex  43331  pr2eldif2  43568  pimxrneun  45499  icccncfext  45902  fourierdlem42  46164  icceuelpartlem  47422  ichnreuop  47459  paireqne  47498  oddprmALTV  47674  rrx2pnedifcoorneor  48637  rrx2linest  48663