Theorem neqned 2994

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

Hypothesis

Ref	Expression
neqned.1	⊢ (𝜑 → ¬ 𝐴 = 𝐵)

Assertion

Ref	Expression
neqned	⊢ (𝜑 → 𝐴 ≠ 𝐵)

Proof of Theorem neqned

Step	Hyp	Ref	Expression
1		neqned.1	. 2 ⊢ (𝜑 → ¬ 𝐴 = 𝐵)
2		df-ne 2988	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	1, 2	sylibr 237	1 ⊢ (𝜑 → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ≠ wne 2987

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 210  df-ne 2988

This theorem is referenced by:  neqne  2995  necon3bi  3013  necon2ai  3016  necon3i  3019  nelne1  3083  nelne2  3084  mteqand  3090  ne0i  4250  nelpr2  4552  nelpr1  4553  otsndisj  5374  enpr2d  8580  sdomdif  8649  2pwne  8657  mapdom2  8672  canthp1lem2  10064  nnneneg  11660  flltnz  13176  wrdlen2i  14295  s3sndisj  14318  isprm2  16016  isprm5  16041  nnoddn2prmb  16140  hashfinmndnn  17920  sgrp2nmndlem5  18086  fincygsubgodd  19227  prmgrpsimpgd  19229  alexsub  22650  ioorf  24177  dvmptdiv  24577  dvtaylp  24965  cos02pilt1  25118  logccne0  25170  isosctrlem1  25404  isosctrlem2  25405  chordthmlem  25418  efrlim  25555  lgsfcl2  25887  lgscllem  25888  lgsval2lem  25891  2sqn0  26018  2sqmod  26020  dchrisumn0  26105  tgbtwnne  26284  tgbtwndiff  26300  tgbtwnconn1lem3  26368  legov3  26392  legso  26393  ncolne1  26419  tglineneq  26438  tglowdim2ln  26445  mirne  26461  miriso  26464  mirhl  26473  mirbtwnhl  26474  symquadlem  26483  krippenlem  26484  midexlem  26486  ragflat3  26500  ragperp  26511  footexALT  26512  footexlem2  26514  colperpexlem2  26525  colperpexlem3  26526  mideulem2  26528  oppne3  26537  outpasch  26549  hlpasch  26550  lmieu  26578  lmicom  26582  axlowdim1  26753  wlkp1lem5  27467  wlkp1lem6  27468  eulerpathpr  28025  nmcfnlbi  29835  strlem1  30033  unidifsnne  30308  fsuppcurry1  30487  fsuppcurry2  30488  divnumden2  30560  xrge0npcan  30728  tocyccntz  30836  ornglmullt  30931  orngrmullt  30932  pidlnz  30991  rhmpreimaprmidl  31035  qsidomlem1  31036  ssmxidl  31050  krull  31051  zarclsint  31225  zarclssn  31226  xrge0iifhom  31290  qqhf  31337  qqhre  31371  esumrnmpt2  31437  carsgclctunlem2  31687  ballotlemi1  31870  ballotlemii  31871  ballotlemfrcn0  31897  plymulx0  31927  signswn0  31940  signswch  31941  itgexpif  31987  repr0  31992  tgoldbachgtda  32042  pconnconn  32591  noseponlem  33284  nosupbnd1lem3  33323  nosupbnd1lem4  33324  nosupbnd1lem5  33325  nosupbnd2lem1  33328  unbdqndv2lem2  33962  knoppndvlem13  33976  sucneqond  34782  finxpreclem2  34807  finxp1o  34809  maxidln0  35483  hdmapip0  39211  metakunt28  39377  metakunt30  39379  remul01  39545  3cubeslem4  39630  3cubes  39631  pellexlem6  39775  scotteld  40954  mnuprdlem2  40981  inaex  41005  n0p  41677  disjrnmpt2  41815  rnmptn0  41850  dstregt0  41912  upbdrech2  41940  xrlexaddrp  41984  infleinflem2  42003  xrralrecnnge  42026  supminfxr2  42108  absimnre  42116  xrpnf  42125  ressioosup  42192  ressiooinf  42194  fmul01lt1lem1  42226  limcperiod  42270  climxrrelem  42391  sinaover2ne0  42510  fperdvper  42561  dvdivbd  42565  itgioocnicc  42619  stirlinglem5  42720  dirker2re  42734  dirkerdenne0  42735  dirkerper  42738  dirkertrigeqlem3  42742  dirkertrigeq  42743  dirkercncflem1  42745  dirkercncflem2  42746  dirkercncflem4  42748  fourierdlem24  42773  fourierdlem25  42774  fourierdlem40  42789  fourierdlem41  42790  fourierdlem42  42791  fourierdlem44  42793  fourierdlem48  42796  fourierdlem49  42797  fourierdlem57  42805  fourierdlem58  42806  fourierdlem59  42807  fourierdlem66  42814  fourierdlem68  42816  fourierdlem74  42822  fourierdlem75  42823  fourierdlem78  42826  fourierdlem80  42828  fourierdlem81  42829  fourierdlem109  42857  elaa2lem  42875  etransclem9  42885  etransclem35  42911  etransclem38  42914  sge0tsms  43019  sge0cl  43020  sge0fodjrnlem  43055  meadjun  43101  meadjiunlem  43104  hoicvr  43187  hoidmvlelem2  43235  hoiqssbllem3  43263  sigardiv  43475  sigarcol  43478  sharhght  43479  prmdvdsfmtnof1lem2  44102  difmodm1lt  44936