Theorem necom 2847

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

Assertion

Ref	Expression
necom	|- ( A =/= B <-> B =/= A )

Proof of Theorem necom

Step	Hyp	Ref	Expression
1		eqcom 2629	. 2 |- ( A = B <-> B = A )
2	1	necon3bii 2846	1 |- ( A =/= B <-> B =/= A )

Syntax hints:   <-> wb 196   =/= wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-ne 2795

This theorem is referenced by:  necomi  2848  necomd  2849  0pss  4013  disjtp2  4252  difprsn1  4330  difprsn2  4331  diftpsn3OLD  4333  prproe  4434  fndmdifcom  6322  fvpr1  6456  fvpr2  6457  fvpr1g  6458  fvtp1  6460  fvtp2  6461  fvtp3  6462  fvtp1g  6463  fvtp2g  6464  fvtp3g  6465  dff14b  6528  f12dfv  6529  f13dfv  6530  orduniorsuc  7030  kmlem3  8974  kmlem4  8975  ac6num  9301  leltne  10127  nn0lt2  11440  xrleltne  11978  fzofzim  12514  elfznelfzo  12573  elfznelfzob  12574  fleqceilz  12653  hashdifpr  13203  hashgt12el  13210  hashgt12el2  13211  cshw0  13540  cshwn  13543  isprm2lem  15394  prm2orodd  15404  cshwsdisj  15805  sgrp2nmndlem5  17416  f1omvdconj  17866  pmtrprfv3  17874  pmtr3ncomlem1  17893  dmdprdd  18398  xrsdsreclblem  19792  xrsdsreclb  19793  ordthaus  21188  hmphindis  21600  angpined  24557  funvtxval0  25897  funvtxval0OLD  25898  snstrvtxval  25929  snstriedgval  25930  nbgrsym  26265  nb3grprlem2  26283  nb3grpr  26284  cusgredg  26320  cplgr3v  26331  1egrvtxdg0  26407  usgr2pthlem  26659  usgr2pth0  26661  2pthdlem1  26826  clwlkclwwlklem2a4  26898  uhgr3cyclex  27042  eupth2lem3lem4  27091  frcond1  27130  frcond4  27134  frgr3v  27139  3vfriswmgr  27142  2pthfrgr  27148  3cyclfrgrrn1  27149  n4cyclfrgr  27155  frgrnbnb  27157  frgrwopreglem4a  27174  ch0pss  28304  pmtrprfv2  29848  esumcvgre  30153  bnj563  30813  cvmsdisj  31252  nosgnn0  31811  noextendlt  31822  nosepne  31831  nosepdm  31834  nosupbnd2lem1  31861  noetalem3  31865  btwnouttr  32131  fscgr  32187  linecom  32257  linerflx2  32258  poimirlem25  33434  divrngidl  33827  lcvbr3  34310  opltn0  34477  atlltn0  34593  2dim  34756  ps-2  34764  islln3  34796  llnexatN  34807  4atlem11  34895  isline4N  35063  lhpex2leN  35299  cdleme48gfv  35825  icccncfext  40100  fourierdlem42  40366  icceuelpartlem  41371  oddprmALTV  41598