Theorem neqned 2940

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  neqne  2941  necon3bi  2959  necon2ai  2962  necon3i  2965  mteqand  3024  nelne1  3030  nelne2  3031  ne0i  4282  rexn0  4437  nelpr2  4598  nelpr1  4599  otsndisj  5465  rnmptn0  6200  enpr2d  8986  sdomdif  9054  2pwne  9062  mapdom2  9077  dif1enlem  9085  infn0  9203  canthp1lem2  10565  nnneneg  12181  flltnz  13732  wrdlen2i  14866  s3sndisj  14891  isprm2  16610  isprm5  16635  nnoddn2prmb  16742  chnind  18545  chnccat  18550  hashfinmndnn  18677  sgrp2nmndlem5  18858  fincygsubgodd  20047  prmgrpsimpgd  20049  ornglmullt  20804  orngrmullt  20805  psdmul  22110  alexsub  23988  ioorf  25518  dvmptdiv  25919  dvtaylp  26318  cos02pilt1  26475  logccne0  26527  isosctrlem1  26768  isosctrlem2  26769  chordthmlem  26782  efrlim  26919  efrlimOLD  26920  lgsfcl2  27254  lgscllem  27255  lgsval2lem  27258  2sqn0  27385  2sqmod  27387  dchrisumn0  27472  noseponlem  27616  nosupbnd1lem3  27662  nosupbnd1lem4  27663  nosupbnd1lem5  27664  nosupbnd2lem1  27667  noinfbnd1lem3  27677  noinfbnd1lem4  27678  noinfbnd1lem5  27679  noetainflem4  27692  cutbdaybnd2lim  27777  bdayfinbndlem1  28447  z12bdaylem1  28450  tgbtwnne  28546  tgbtwndiff  28562  tgbtwnconn1lem3  28630  legov3  28654  legso  28655  ncolne1  28681  tglineneq  28700  tglowdim2ln  28707  mirne  28723  miriso  28726  mirhl  28735  mirbtwnhl  28736  symquadlem  28745  krippenlem  28746  midexlem  28748  ragflat3  28762  ragperp  28773  footexALT  28774  footexlem2  28776  colperpexlem2  28787  colperpexlem3  28788  mideulem2  28790  oppne3  28799  outpasch  28811  hlpasch  28812  lmieu  28840  lmicom  28844  axlowdim1  29016  wlkp1lem5  29733  wlkp1lem6  29734  eulerpathpr  30299  nmcfnlbi  32112  strlem1  32310  unidifsnne  32595  fsuppcurry1  32786  fsuppcurry2  32787  hashpss  32872  divnumden2  32879  xrge0npcan  33085  tocyccntz  33210  elrgspnlem4  33311  fracfld  33374  pidlnz  33441  drngidl  33498  drngidlhash  33499  rhmpreimaprmidl  33516  qsidomlem1  33517  qsnzr  33520  mxidlirredi  33536  mxidlirred  33537  ssmxidl  33539  krull  33544  krullndrng  33546  qsdrng  33562  rprmasso2  33591  rprmirred  33596  pidufd  33608  1arithufdlem3  33611  mplmulmvr  33688  esplyind  33724  vietadeg1  33727  exsslsb  33746  constrextdg2lem  33898  constrext2chnlem  33900  2sqr3nconstr  33931  cos9thpinconstrlem2  33940  zarclsint  34022  zarclssn  34023  xrge0iifhom  34087  qqhf  34136  qqhre  34170  esumrnmpt2  34218  carsgclctunlem2  34469  ballotlemi1  34653  ballotlemii  34654  ballotlemfrcn0  34680  plymulx0  34697  signswn0  34710  signswch  34711  itgexpif  34756  repr0  34761  tgoldbachgtda  34811  noinfepfnregs  35282  pconnconn  35419  unbdqndv2lem2  36768  knoppndvlem13  36782  sucneqond  37677  finxpreclem2  37702  finxp1o  37704  maxidln0  38357  hdmapip0  42352  fldhmf1  42521  hashscontpow1  42552  aks6d1c6lem4  42604  aks6d1c7lem1  42611  remul01  42838  3cubeslem4  43120  3cubes  43121  pellexlem6  43265  nlimsuc  43871  scotteld  44676  mnuprdlem2  44703  inaex  44727  n0p  45479  disjrnmpt2  45621  dstregt0  45718  upbdrech2  45744  xrlexaddrp  45785  infleinflem2  45803  xrralrecnnge  45822  supminfxr2  45901  absimnre  45908  xrpnf  45917  ressioosup  45989  ressiooinf  45991  fmul01lt1lem1  46018  limcperiod  46062  climxrrelem  46181  sinaover2ne0  46300  fperdvper  46351  dvdivbd  46355  itgioocnicc  46409  stirlinglem5  46510  dirker2re  46524  dirkerdenne0  46525  dirkerper  46528  dirkertrigeqlem3  46532  dirkertrigeq  46533  dirkercncflem1  46535  dirkercncflem2  46536  dirkercncflem4  46538  fourierdlem24  46563  fourierdlem25  46564  fourierdlem40  46579  fourierdlem41  46580  fourierdlem42  46581  fourierdlem44  46583  fourierdlem48  46586  fourierdlem49  46587  fourierdlem57  46595  fourierdlem58  46596  fourierdlem59  46597  fourierdlem66  46604  fourierdlem68  46606  fourierdlem74  46612  fourierdlem75  46613  fourierdlem78  46616  fourierdlem80  46618  fourierdlem81  46619  fourierdlem109  46647  elaa2lem  46665  etransclem9  46675  etransclem35  46701  etransclem38  46704  sge0tsms  46812  sge0cl  46813  sge0fodjrnlem  46848  meadjun  46894  meadjiunlem  46897  hoicvr  46980  hoidmvlelem2  47028  hoiqssbllem3  47056  sigardiv  47293  sigarcol  47296  sharhght  47297  chnsubseq  47312  difltmodne  47776  minusmodnep2tmod  47787  modm1p1ne  47804  prmdvdsfmtnof1lem2  48019  gpg3kgrtriexlem5  48521  fucofvalne  49758  fullthinc  49883  euendfunc2  49960