Theorem neqned 2942

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1534   ≠ wne 2935

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 2936

This theorem is referenced by:  neqne  2943  necon3bi  2962  necon2ai  2965  necon3i  2968  mteqand  3028  nelne1  3034  nelne2  3035  ne0i  4330  rexn0  4506  nelpr2  4651  nelpr1  4652  otsndisj  5515  rnmptn0  6242  enpr2d  9065  enpr2dOLD  9066  sdomdif  9141  2pwne  9149  mapdom2  9164  dif1enlem  9172  dif1enlemOLD  9173  infn0  9323  canthp1lem2  10668  nnneneg  12269  flltnz  13800  wrdlen2i  14917  s3sndisj  14938  isprm2  16644  isprm5  16669  nnoddn2prmb  16773  hashfinmndnn  18702  sgrp2nmndlem5  18872  fincygsubgodd  20060  prmgrpsimpgd  20062  psdmul  22077  alexsub  23936  ioorf  25489  dvmptdiv  25893  dvtaylp  26292  cos02pilt1  26447  logccne0  26499  isosctrlem1  26737  isosctrlem2  26738  chordthmlem  26751  efrlim  26888  efrlimOLD  26889  lgsfcl2  27223  lgscllem  27224  lgsval2lem  27227  2sqn0  27354  2sqmod  27356  dchrisumn0  27441  noseponlem  27584  nosupbnd1lem3  27630  nosupbnd1lem4  27631  nosupbnd1lem5  27632  nosupbnd2lem1  27635  noinfbnd1lem3  27645  noinfbnd1lem4  27646  noinfbnd1lem5  27647  noetainflem4  27660  scutbdaybnd2lim  27737  tgbtwnne  28281  tgbtwndiff  28297  tgbtwnconn1lem3  28365  legov3  28389  legso  28390  ncolne1  28416  tglineneq  28435  tglowdim2ln  28442  mirne  28458  miriso  28461  mirhl  28470  mirbtwnhl  28471  symquadlem  28480  krippenlem  28481  midexlem  28483  ragflat3  28497  ragperp  28508  footexALT  28509  footexlem2  28511  colperpexlem2  28522  colperpexlem3  28523  mideulem2  28525  oppne3  28534  outpasch  28546  hlpasch  28547  lmieu  28575  lmicom  28579  axlowdim1  28757  wlkp1lem5  29478  wlkp1lem6  29479  eulerpathpr  30037  nmcfnlbi  31849  strlem1  32047  unidifsnne  32317  fsuppcurry1  32491  fsuppcurry2  32492  divnumden2  32563  xrge0npcan  32732  tocyccntz  32843  ornglmullt  32962  orngrmullt  32963  pidlnz  33027  drngidl  33084  drngidlhash  33085  rhmpreimaprmidl  33103  qsidomlem1  33104  qsnzr  33107  mxidlirredi  33120  mxidlirred  33121  ssmxidl  33123  krull  33127  qsdrng  33144  zarclsint  33409  zarclssn  33410  xrge0iifhom  33474  qqhf  33523  qqhre  33557  esumrnmpt2  33623  carsgclctunlem2  33875  ballotlemi1  34058  ballotlemii  34059  ballotlemfrcn0  34085  plymulx0  34115  signswn0  34128  signswch  34129  itgexpif  34174  repr0  34179  tgoldbachgtda  34229  pconnconn  34777  unbdqndv2lem2  35921  knoppndvlem13  35935  sucneqond  36780  finxpreclem2  36805  finxp1o  36807  maxidln0  37453  hdmapip0  41325  fldhmf1  41498  hashscontpow1  41525  metakunt28  41604  metakunt30  41606  remul01  41884  3cubeslem4  42031  3cubes  42032  pellexlem6  42176  nlimsuc  42794  scotteld  43606  mnuprdlem2  43633  inaex  43657  n0p  44330  disjrnmpt2  44484  dstregt0  44586  upbdrech2  44613  xrlexaddrp  44657  infleinflem2  44676  xrralrecnnge  44695  supminfxr2  44774  absimnre  44782  xrpnf  44791  ressioosup  44863  ressiooinf  44865  fmul01lt1lem1  44895  limcperiod  44939  climxrrelem  45060  sinaover2ne0  45179  fperdvper  45230  dvdivbd  45234  itgioocnicc  45288  stirlinglem5  45389  dirker2re  45403  dirkerdenne0  45404  dirkerper  45407  dirkertrigeqlem3  45411  dirkertrigeq  45412  dirkercncflem1  45414  dirkercncflem2  45415  dirkercncflem4  45417  fourierdlem24  45442  fourierdlem25  45443  fourierdlem40  45458  fourierdlem41  45459  fourierdlem42  45460  fourierdlem44  45462  fourierdlem48  45465  fourierdlem49  45466  fourierdlem57  45474  fourierdlem58  45475  fourierdlem59  45476  fourierdlem66  45483  fourierdlem68  45485  fourierdlem74  45491  fourierdlem75  45492  fourierdlem78  45495  fourierdlem80  45497  fourierdlem81  45498  fourierdlem109  45526  elaa2lem  45544  etransclem9  45554  etransclem35  45580  etransclem38  45583  sge0tsms  45691  sge0cl  45692  sge0fodjrnlem  45727  meadjun  45773  meadjiunlem  45776  hoicvr  45859  hoidmvlelem2  45907  hoiqssbllem3  45935  sigardiv  46172  sigarcol  46175  sharhght  46176  prmdvdsfmtnof1lem2  46848  difmodm1lt  47518  fullthinc  47975