Theorem neqned 2945

Description: If it is not the case that two classes are equal, then they are unequal. Converse of neneqd 2943. One-way deduction form of df-ne 2939. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2965. (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 2939	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	1, 2	sylibr 233	1 ⊢ (𝜑 → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2938

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 206  df-ne 2939

This theorem is referenced by:  neqne  2946  necon3bi  2965  necon2ai  2968  necon3i  2971  mteqand  3031  nelne1  3037  nelne2  3038  ne0i  4335  rexn0  4511  nelpr2  4656  nelpr1  4657  otsndisj  5520  rnmptn0  6244  enpr2d  9053  enpr2dOLD  9054  sdomdif  9129  2pwne  9137  mapdom2  9152  dif1enlem  9160  dif1enlemOLD  9161  infn0  9311  canthp1lem2  10652  nnneneg  12253  flltnz  13782  wrdlen2i  14899  s3sndisj  14920  isprm2  16625  isprm5  16650  nnoddn2prmb  16752  hashfinmndnn  18678  sgrp2nmndlem5  18848  fincygsubgodd  20025  prmgrpsimpgd  20027  alexsub  23771  ioorf  25324  dvmptdiv  25725  dvtaylp  26116  cos02pilt1  26269  logccne0  26321  isosctrlem1  26557  isosctrlem2  26558  chordthmlem  26571  efrlim  26708  lgsfcl2  27040  lgscllem  27041  lgsval2lem  27044  2sqn0  27171  2sqmod  27173  dchrisumn0  27258  noseponlem  27401  nosupbnd1lem3  27447  nosupbnd1lem4  27448  nosupbnd1lem5  27449  nosupbnd2lem1  27452  noinfbnd1lem3  27462  noinfbnd1lem4  27463  noinfbnd1lem5  27464  noetainflem4  27477  scutbdaybnd2lim  27553  tgbtwnne  28006  tgbtwndiff  28022  tgbtwnconn1lem3  28090  legov3  28114  legso  28115  ncolne1  28141  tglineneq  28160  tglowdim2ln  28167  mirne  28183  miriso  28186  mirhl  28195  mirbtwnhl  28196  symquadlem  28205  krippenlem  28206  midexlem  28208  ragflat3  28222  ragperp  28233  footexALT  28234  footexlem2  28236  colperpexlem2  28247  colperpexlem3  28248  mideulem2  28250  oppne3  28259  outpasch  28271  hlpasch  28272  lmieu  28300  lmicom  28304  axlowdim1  28482  wlkp1lem5  29199  wlkp1lem6  29200  eulerpathpr  29758  nmcfnlbi  31570  strlem1  31768  unidifsnne  32038  fsuppcurry1  32215  fsuppcurry2  32216  divnumden2  32289  xrge0npcan  32460  tocyccntz  32571  ornglmullt  32693  orngrmullt  32694  pidlnz  32760  drngidl  32823  drngidlhash  32824  rhmpreimaprmidl  32842  qsidomlem1  32843  qsnzr  32846  mxidlirredi  32859  mxidlirred  32860  ssmxidl  32862  krull  32866  qsdrng  32883  zarclsint  33148  zarclssn  33149  xrge0iifhom  33213  qqhf  33262  qqhre  33296  esumrnmpt2  33362  carsgclctunlem2  33614  ballotlemi1  33797  ballotlemii  33798  ballotlemfrcn0  33824  plymulx0  33854  signswn0  33867  signswch  33868  itgexpif  33914  repr0  33919  tgoldbachgtda  33969  pconnconn  34518  unbdqndv2lem2  35691  knoppndvlem13  35705  sucneqond  36551  finxpreclem2  36576  finxp1o  36578  maxidln0  37218  hdmapip0  41091  fldhmf1  41263  metakunt28  41320  metakunt30  41322  remul01  41584  3cubeslem4  41731  3cubes  41732  pellexlem6  41876  nlimsuc  42496  scotteld  43309  mnuprdlem2  43336  inaex  43360  n0p  44033  disjrnmpt2  44187  dstregt0  44291  upbdrech2  44318  xrlexaddrp  44362  infleinflem2  44381  xrralrecnnge  44400  supminfxr2  44479  absimnre  44487  xrpnf  44496  ressioosup  44568  ressiooinf  44570  fmul01lt1lem1  44600  limcperiod  44644  climxrrelem  44765  sinaover2ne0  44884  fperdvper  44935  dvdivbd  44939  itgioocnicc  44993  stirlinglem5  45094  dirker2re  45108  dirkerdenne0  45109  dirkerper  45112  dirkertrigeqlem3  45116  dirkertrigeq  45117  dirkercncflem1  45119  dirkercncflem2  45120  dirkercncflem4  45122  fourierdlem24  45147  fourierdlem25  45148  fourierdlem40  45163  fourierdlem41  45164  fourierdlem42  45165  fourierdlem44  45167  fourierdlem48  45170  fourierdlem49  45171  fourierdlem57  45179  fourierdlem58  45180  fourierdlem59  45181  fourierdlem66  45188  fourierdlem68  45190  fourierdlem74  45196  fourierdlem75  45197  fourierdlem78  45200  fourierdlem80  45202  fourierdlem81  45203  fourierdlem109  45231  elaa2lem  45249  etransclem9  45259  etransclem35  45285  etransclem38  45288  sge0tsms  45396  sge0cl  45397  sge0fodjrnlem  45432  meadjun  45478  meadjiunlem  45481  hoicvr  45564  hoidmvlelem2  45612  hoiqssbllem3  45640  sigardiv  45877  sigarcol  45880  sharhght  45881  prmdvdsfmtnof1lem2  46553  difmodm1lt  47297  fullthinc  47755