Theorem nesym 2850

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

Assertion

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

Proof of Theorem nesym

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

Syntax hints:   -. wn 3   <-> wb 196   = wceq 1483   =/= 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:  0neqopab  6698  fiming  8404  wemapsolem  8455  nn01to3  11781  xrltlen  11979  sgnn  13834  pwm1geoser  14600  isprm3  15396  lspsncv0  19146  uvcvv0  20129  fvmptnn04if  20654  chfacfisf  20659  chfacfisfcpmat  20660  trfbas  21648  fbunfip  21673  trfil2  21691  iundisj2  23317  pthdlem2lem  26663  fusgr2wsp2nb  27198  iundisj2f  29403  iundisj2fi  29556  cvmscld  31255  nosupbnd2lem1  31861  poimirlem25  33434  hlrelat5N  34687  cmpfiiin  37260  gneispace  38432  iblcncfioo  40194  fourierdlem82  40405  elprneb  41296  fzopredsuc  41333  iccpartiltu  41358