Theorem neqned 2939

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2932

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 207  df-ne 2933

This theorem is referenced by:  neqne  2940  necon3bi  2958  necon2ai  2961  necon3i  2964  mteqand  3023  nelne1  3029  nelne2  3030  ne0i  4316  rexn0  4486  nelpr2  4629  nelpr1  4630  otsndisj  5494  rnmptn0  6233  enpr2d  9061  enpr2dOLD  9062  sdomdif  9137  2pwne  9145  mapdom2  9160  dif1enlem  9168  dif1enlemOLD  9169  infn0  9310  canthp1lem2  10665  nnneneg  12273  flltnz  13826  wrdlen2i  14959  s3sndisj  14984  isprm2  16699  isprm5  16724  nnoddn2prmb  16831  hashfinmndnn  18727  sgrp2nmndlem5  18905  fincygsubgodd  20093  prmgrpsimpgd  20095  psdmul  22102  alexsub  23981  ioorf  25524  dvmptdiv  25928  dvtaylp  26328  cos02pilt1  26485  logccne0  26537  isosctrlem1  26778  isosctrlem2  26779  chordthmlem  26792  efrlim  26929  efrlimOLD  26930  lgsfcl2  27264  lgscllem  27265  lgsval2lem  27268  2sqn0  27395  2sqmod  27397  dchrisumn0  27482  noseponlem  27626  nosupbnd1lem3  27672  nosupbnd1lem4  27673  nosupbnd1lem5  27674  nosupbnd2lem1  27677  noinfbnd1lem3  27687  noinfbnd1lem4  27688  noinfbnd1lem5  27689  noetainflem4  27702  scutbdaybnd2lim  27779  tgbtwnne  28415  tgbtwndiff  28431  tgbtwnconn1lem3  28499  legov3  28523  legso  28524  ncolne1  28550  tglineneq  28569  tglowdim2ln  28576  mirne  28592  miriso  28595  mirhl  28604  mirbtwnhl  28605  symquadlem  28614  krippenlem  28615  midexlem  28617  ragflat3  28631  ragperp  28642  footexALT  28643  footexlem2  28645  colperpexlem2  28656  colperpexlem3  28657  mideulem2  28659  oppne3  28668  outpasch  28680  hlpasch  28681  lmieu  28709  lmicom  28713  axlowdim1  28884  wlkp1lem5  29603  wlkp1lem6  29604  eulerpathpr  30167  nmcfnlbi  31979  strlem1  32177  unidifsnne  32463  fsuppcurry1  32648  fsuppcurry2  32649  hashpss  32734  divnumden2  32740  chnind  32937  xrge0npcan  32961  tocyccntz  33101  elrgspnlem4  33186  fracfld  33248  ornglmullt  33275  orngrmullt  33276  pidlnz  33337  drngidl  33394  drngidlhash  33395  rhmpreimaprmidl  33412  qsidomlem1  33413  qsnzr  33416  mxidlirredi  33432  mxidlirred  33433  ssmxidl  33435  krull  33440  krullndrng  33442  qsdrng  33458  rprmasso2  33487  rprmirred  33492  pidufd  33504  1arithufdlem3  33507  exsslsb  33582  constrextdg2lem  33728  constrext2chnlem  33730  2sqr3nconstr  33761  zarclsint  33849  zarclssn  33850  xrge0iifhom  33914  qqhf  33963  qqhre  33997  esumrnmpt2  34045  carsgclctunlem2  34297  ballotlemi1  34481  ballotlemii  34482  ballotlemfrcn0  34508  plymulx0  34525  signswn0  34538  signswch  34539  itgexpif  34584  repr0  34589  tgoldbachgtda  34639  pconnconn  35199  unbdqndv2lem2  36474  knoppndvlem13  36488  sucneqond  37329  finxpreclem2  37354  finxp1o  37356  maxidln0  38015  hdmapip0  41880  fldhmf1  42049  hashscontpow1  42080  aks6d1c6lem4  42132  aks6d1c7lem1  42139  metakunt28  42191  metakunt30  42193  remul01  42397  3cubeslem4  42659  3cubes  42660  pellexlem6  42804  nlimsuc  43412  scotteld  44218  mnuprdlem2  44245  inaex  44269  n0p  45017  disjrnmpt2  45160  dstregt0  45258  upbdrech2  45285  xrlexaddrp  45327  infleinflem2  45346  xrralrecnnge  45365  supminfxr2  45444  absimnre  45451  xrpnf  45460  ressioosup  45532  ressiooinf  45534  fmul01lt1lem1  45561  limcperiod  45605  climxrrelem  45726  sinaover2ne0  45845  fperdvper  45896  dvdivbd  45900  itgioocnicc  45954  stirlinglem5  46055  dirker2re  46069  dirkerdenne0  46070  dirkerper  46073  dirkertrigeqlem3  46077  dirkertrigeq  46078  dirkercncflem1  46080  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem24  46108  fourierdlem25  46109  fourierdlem40  46124  fourierdlem41  46125  fourierdlem42  46126  fourierdlem44  46128  fourierdlem48  46131  fourierdlem49  46132  fourierdlem57  46140  fourierdlem58  46141  fourierdlem59  46142  fourierdlem66  46149  fourierdlem68  46151  fourierdlem74  46157  fourierdlem75  46158  fourierdlem78  46161  fourierdlem80  46163  fourierdlem81  46164  fourierdlem109  46192  elaa2lem  46210  etransclem9  46220  etransclem35  46246  etransclem38  46249  sge0tsms  46357  sge0cl  46358  sge0fodjrnlem  46393  meadjun  46439  meadjiunlem  46442  hoicvr  46525  hoidmvlelem2  46573  hoiqssbllem3  46601  sigardiv  46838  sigarcol  46841  sharhght  46842  difltmodne  47319  minusmodnep2tmod  47330  prmdvdsfmtnof1lem2  47547  gpg3kgrtriexlem5  48037  difmodm1lt  48450  fucofvalne  49184  fullthinc  49284  euendfunc2  49360