Theorem nesym 2729

Description: Characterization of inequality in terms of reversed equality (see bicom 200). (Contributed by BJ, 7-Jul-2018.)

Assertion

Ref	Expression
nesym

Proof of Theorem nesym

Step	Hyp	Ref	Expression
1		eqcom 2466	. 2
2	1	necon3abii 2717	1

Syntax hints:  -.wn 3  <->wb 184  =wceq 1395  =/=wne 2652

This theorem is referenced by:  nesymiOLD  2731  nesymirOLD  2733  0neqopab  6341  wemapsolem  7996  nn01to3  11204  xrltlen  11381  sgnn  12927  isprm3  14226  lspsncv0  17792  uvcvv0  18821  fvmptnn04if  19350  chfacfisf  19355  chfacfisfcpmat  19356  trfbas  20345  fbunfip  20370  trfil2  20388  iundisj2  21959  2pthfrgra  25011  frgrawopreglem3  25046  usg2spot2nb  25065  iundisj2f  27449  iundisj2fi  27602  cvmscld  28718  cmpfiiin  30629  iblcncfioo  31777  fourierdlem82  31971  hlrelat5N  35125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-cleq 2449  df-ne 2654