Theorem neqned 2954

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1550   ≠ wne 2947

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 209  df-ne 2948

This theorem is referenced by:  neqne  2955  necon3bi  2973  necon2ai  2976  necon3i  2979  mteqand  3038  nelne1  3044  nelne2  3045  ne0i  4284  rexn0  4440  nelpr2  4602  nelpr1  4603  otsndisj  5478  rnmptn0  6216  enpr2d  9014  sdomdif  9082  2pwne  9090  mapdom2  9105  dif1enlem  9113  infn0  9231  canthp1lem2  10597  nnneneg  12234  flltnz  13807  wrdlen2i  14941  s3sndisj  14966  isprm2  16688  isprm5  16714  nnoddn2prmb  16821  chnind  18625  chnccat  18630  hashfinmndnn  18757  sgrp2nmndlem5  18938  fincygsubgodd  20126  prmgrpsimpgd  20128  ornglmullt  20887  orngrmullt  20888  psdmul  22200  alexsub  24074  ioorf  25604  dvmptdiv  26005  dvtaylp  26399  cos02pilt1  26557  logccne0  26609  isosctrlem1  26849  isosctrlem2  26850  chordthmlem  26863  efrlim  27000  lgsfcl2  27333  lgscllem  27334  lgsval2lem  27337  2sqn0  27464  2sqmod  27466  dchrisumn0  27551  noseponlem  27694  nosupbnd1lem3  27740  nosupbnd1lem4  27741  nosupbnd1lem5  27742  nosupbnd2lem1  27745  noinfbnd1lem3  27755  noinfbnd1lem4  27756  noinfbnd1lem5  27757  noetainflem4  27770  cutbdaybnd2lim  27856  bdayfinbndlem1  28526  z12bdaylem1  28529  tgbtwnne  28625  tgbtwndiff  28641  tgbtwnconn1lem3  28709  legov3  28733  legso  28734  ncolne1  28760  tglineneq  28779  tglowdim2ln  28786  mirne  28802  miriso  28805  mirhl  28814  mirbtwnhl  28815  symquadlem  28824  krippenlem  28825  midexlem  28827  ragflat3  28841  ragperp  28852  footexALT  28853  footexlem2  28855  colperpexlem2  28866  colperpexlem3  28867  mideulem2  28869  oppne3  28878  outpasch  28890  hlpasch  28891  lmieu  28919  lmicom  28923  axlowdim1  29095  wlkp1lem5  29811  wlkp1lem6  29812  eulerpathpr  30377  nmcfnlbi  32190  strlem1  32388  unidifsnne  32673  fsuppcurry1  32865  fsuppcurry2  32866  hashpss  32950  divnumden2  32957  xrge0npcan  33148  tocyccntz  33274  elrgspnlem4  33375  fracfld  33441  pidlnz  33508  drngidl  33565  drngidlhash  33566  rhmpreimaprmidl  33583  qsidomlem1  33584  qsnzr  33587  mxidlirredi  33603  mxidlirred  33604  ssmxidl  33606  krull  33611  krullndrng  33613  qsdrng  33629  dflringlem  33634  rprmasso2  33666  rprmirred  33671  pidufd  33683  1arithufdlem3  33686  mplmulmvr  33780  esplyind  33816  vietadeg1  33819  exsslsb  33838  constrextdg2lem  33989  constrext2chnlem  33991  2sqr3nconstr  34022  cos9thpinconstrlem2  34031  zarclsint  34113  zarclssn  34114  xrge0iifhom  34178  qqhf  34227  qqhre  34261  esumrnmpt2  34309  carsgclctunlem2  34560  ballotlemi1  34744  ballotlemii  34745  ballotlemfrcn0  34771  plymulx0  34788  signswn0  34801  signswch  34802  itgexpif  34847  repr0  34852  tgoldbachgtda  34902  morleylemrneab  34912  noinfepfnregs  35373  pconnconn  35519  unbdqndv2lem2  36886  knoppndvlem13  36900  qdiff  37757  sucneqond  37797  finxpreclem2  37822  finxp1o  37824  maxidln0  38482  hdmapip0  42477  fldhmf1  42645  hashscontpow1  42676  aks6d1c6lem4  42728  aks6d1c7lem1  42735  remul01  42954  3cubeslem4  43208  3cubes  43209  pellexlem6  43349  nlimsuc  43955  scotteld  44760  mnuprdlem2  44787  inaex  44811  n0p  45563  disjrnmpt2  45704  dstregt0  45799  upbdrech2  45825  xrlexaddrp  45866  infleinflem2  45884  xrralrecnnge  45903  supminfxr2  45981  absimnre  45988  xrpnf  45997  ressioosup  46069  ressiooinf  46071  fmul01lt1lem1  46098  limcperiod  46142  climxrrelem  46261  sinaover2ne0  46380  fperdvper  46431  dvdivbd  46435  itgioocnicc  46489  stirlinglem5  46590  dirker2re  46604  dirkerdenne0  46605  dirkerper  46608  dirkertrigeqlem3  46612  dirkertrigeq  46613  dirkercncflem1  46615  dirkercncflem2  46616  dirkercncflem4  46618  fourierdlem24  46643  fourierdlem25  46644  fourierdlem40  46659  fourierdlem41  46660  fourierdlem42  46661  fourierdlem44  46663  fourierdlem48  46666  fourierdlem49  46667  fourierdlem57  46675  fourierdlem58  46676  fourierdlem59  46677  fourierdlem66  46684  fourierdlem68  46686  fourierdlem74  46692  fourierdlem75  46693  fourierdlem78  46696  fourierdlem80  46698  fourierdlem81  46699  fourierdlem109  46727  elaa2lem  46745  etransclem9  46755  etransclem35  46781  etransclem38  46784  sge0tsms  46892  sge0cl  46893  sge0fodjrnlem  46928  meadjun  46974  meadjiunlem  46977  hoicvr  47060  hoidmvlelem2  47108  hoiqssbllem3  47136  sigardiv  47373  sigarcol  47376  sharhght  47377  chnsubseq  47394  difltmodne  47880  minusmodnep2tmod  47891  modm1p1ne  47908  prmdvdsfmtnof1lem2  48132  gpg3kgrtriexlem5  48647  fucofvalne  49884  fullthinc  50009  euendfunc2  50086