Theorem neqned 2801

Description: If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2799. One-way deduction form of df-ne 2795. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2820. (Revised by Wolf Lammen, 22-Nov-2019.)

Hypothesis

Ref	Expression
neqned.1	|- ( ph -> -. A = B )

Assertion

Ref	Expression
neqned	|- ( ph -> A =/= B )

Proof of Theorem neqned

Step	Hyp	Ref	Expression
1		neqned.1	. 2 |- ( ph -> -. A = B )
2		df-ne 2795	. 2 |- ( A =/= B <-> -. A = B )
3	1, 2	sylibr 224	1 |- ( ph -> A =/= B )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1483   =/= wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-ne 2795

This theorem is referenced by:  neqne  2802  necon3bi  2820  necon2ai  2823  necon3i  2826  ne0i  3921  otsndisj  4979  sdomdif  8108  2pwne  8116  mapdom2  8131  canthp1lem2  9475  xrge0neqmnf  12276  flltnz  12612  wrdlen2i  13686  s3sndisj  13706  isprm2  15395  isprm5  15419  nnoddn2prmb  15518  sgrp2nmndlem5  17416  maducoeval2  20446  alexsub  21849  ioorf  23341  dvmptdiv  23737  dvtaylp  24124  logccne0  24325  isosctrlem1  24548  isosctrlem2  24549  chordthmlem  24559  efrlim  24696  lgsfcl2  25028  lgscllem  25029  lgsval2lem  25032  dchrisumn0  25210  tgbtwnne  25385  tgbtwndiff  25401  tgbtwnconn1lem3  25469  legov3  25493  legso  25494  ncolne1  25520  tglineneq  25539  tglowdim2ln  25546  mirne  25562  miriso  25565  mirhl  25574  mirbtwnhl  25575  symquadlem  25584  krippenlem  25585  midexlem  25587  ragflat3  25601  ragperp  25612  footex  25613  colperpexlem2  25623  colperpexlem3  25624  mideulem2  25626  oppne3  25635  outpasch  25647  hlpasch  25648  lmieu  25676  lmicom  25680  axlowdim1  25839  nbgrssovtx  26260  wlkp1lem5  26574  wlkp1lem6  26575  eulerpathpr  27100  nmcfnlbi  28911  strlem1  29109  divnumden2  29564  2sqn0  29646  2sqmod  29648  xrge0npcan  29694  ornglmullt  29807  orngrmullt  29808  xrge0iifhom  29983  qqhf  30030  qqhre  30064  esumrnmpt2  30130  carsgclctunlem2  30381  ballotlemi1  30564  ballotlemii  30565  ballotlemfrcn0  30591  plymulx0  30624  signswn0  30637  signswch  30638  signstfvneq0  30649  itgexpif  30684  repr0  30689  tgoldbachgtda  30739  pconnconn  31213  noseponlem  31817  nosupbnd1lem3  31856  nosupbnd1lem4  31857  nosupbnd1lem5  31858  nosupbnd2lem1  31861  unbdqndv2lem2  32501  knoppndvlem13  32515  sucneqond  33213  finxpreclem2  33227  finxp1o  33229  maxidln0  33844  hdmapip0  37207  pellexlem6  37398  n0p  39209  nelpr2  39261  nelpr1  39262  disjrnmpt2  39375  rnmptn0  39413  dstregt0  39493  upbdrech2  39522  xrlexaddrp  39568  infleinflem2  39587  xrralrecnnge  39613  supminfxr2  39699  absimnre  39707  ressioosup  39782  ressiooinf  39784  fmul01lt1lem1  39816  limcperiod  39860  climxrrelem  39981  sinaover2ne0  40079  fperdvper  40133  dvdivbd  40138  itgioocnicc  40193  stirlinglem5  40295  dirker2re  40309  dirkerdenne0  40310  dirkerper  40313  dirkertrigeqlem3  40317  dirkertrigeq  40318  dirkercncflem1  40320  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem24  40348  fourierdlem25  40349  fourierdlem40  40364  fourierdlem41  40365  fourierdlem42  40366  fourierdlem44  40368  fourierdlem48  40371  fourierdlem49  40372  fourierdlem57  40380  fourierdlem58  40381  fourierdlem59  40382  fourierdlem66  40389  fourierdlem68  40391  fourierdlem74  40397  fourierdlem75  40398  fourierdlem78  40401  fourierdlem80  40403  fourierdlem81  40404  fourierdlem109  40432  elaa2lem  40450  etransclem9  40460  etransclem35  40486  etransclem38  40489  sge0tsms  40597  sge0cl  40598  sge0fodjrnlem  40633  meadjun  40679  meadjiunlem  40682  hoicvr  40762  hoidmvlelem2  40810  hoiqssbllem3  40838  sigardiv  41050  sigarcol  41053  sharhght  41054  prmdvdsfmtnof1lem2  41497  difmodm1lt  42317