Theorem neqned 2966

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2959

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2960

This theorem is used by:  neqne  2967  necon3bi  2985  necon2ai  2988  necon3i  2991  mteqand  3050  nelne1  3056  nelne2  3057  ne0i  4290  rexn0  4455  nelpr2  4614  nelpr1  4615  otsndisj  5496  rnmptn0  6258  enpr2d  9104  sdomdif  9172  2pwne  9180  mapdom2  9195  dif1enlem  9203  infn0  9322  scotteld  9974  canthp1lem2  10765  nnneneg  12400  flltnz  13978  hashpss  14581  wrdlen2i  15122  s3sndisj  15149  isprm2  16886  isprm5  16912  nnoddn2prmb  17020  chnind  18824  chnccat  18829  hashfinmndnn  18970  sgrp2nmndlem5  19157  fincygsubgodd  20358  prmgrpsimpgd  20360  ornglmullt  21156  orngrmullt  21157  pidlnz  21558  drngidl  21569  rhmpreimaprmidl  21665  qsidomlem1  21666  qsnzr  21669  psdmul  22517  alexsub  24394  ioorf  25924  dvmptdiv  26324  plyn0mulidp  26632  dvtaylp  26727  cos02pilt1  26884  logccne0  26936  isosctrlem1  27176  isosctrlem2  27177  chordthmlem  27190  efrlim  27327  lgsfcl2  27660  lgscllem  27661  lgsval2lem  27664  2sqn0  27791  2sqmod  27793  dchrisumn0  27878  nna4b4nsq  28020  flt4ALT  28022  noseponlem  28051  nosupbnd1lem3  28097  nosupbnd1lem4  28098  nosupbnd1lem5  28099  nosupbnd2lem1  28102  noinfbnd1lem3  28112  noinfbnd1lem4  28113  noinfbnd1lem5  28114  noetainflem4  28127  cutbdaybnd2lim  28213  bdayfinbndlem1  28883  z12bdaylem1  28886  tgbtwnne  28983  tgbtwndiff  28999  tgbtwnconn1lem3  29067  legov3  29091  legso  29092  ncolne1  29123  tglineneq  29143  tglowdim2ln  29150  mirne  29169  miriso  29172  mirhl  29181  mirbtwnhl  29182  symquadlem  29191  krippenlem  29192  midexlem  29194  symquadprlnglem  29195  ragflat3  29211  ragperp  29222  footexALT  29223  footexlem2  29225  colperpexlem2  29237  colperpexlem3  29238  mideulem2  29240  oppne3  29249  outpasch  29263  hlpasch  29264  plngrotlem1  29295  lmieu  29319  lmicom  29323  tgaaddcpbllem1  29379  tgaaddcpbllem2  29380  angmgmaddeu1  29409  angmgmaddov2lem  29417  prlngmolem1  29460  prlngmo2  29464  prlngplngtr  29467  prlnginn0  29468  prlngmid2  29469  symquadprlng  29470  quadcgrprlng  29474  axlowdim1  29567  wlkp1lem5  30286  wlkp1lem6  30287  eulerpathpr  30871  nmcfnlbi  32684  strlem1  32882  tgextancd  33098  tgextalem1inag  33100  tgextamirnhl  33102  unidifsnne  33204  fsuppcurry1  33386  fsuppcurry2  33387  divnumden2  33477  xrge0npcan  33651  tocyccntz  33775  elrgspnlem4  33876  fracfld  33940  drngidlhash  34053  mxidlirredi  34066  mxidlirred  34067  ssmxidl  34069  krull  34073  krullndrng  34075  qsdrng  34091  dflringlem  34096  rprmasso2  34128  rprmirred  34133  pidufd  34145  1arithufdlem3  34148  mplmulmvr  34241  esplyind  34277  vietadeg1  34280  exsslsb  34299  constrextdg2lem  34450  constrext2chnlem  34452  2sqr3nconstr  34483  cos9thpinconstrlem2  34492  zarclsint  34574  zarclssn  34575  xrge0iifhom  34639  qqhf  34688  qqhre  34722  esumrnmpt2  34770  carsgclctunlem2  35021  ballotlemi1  35205  ballotlemii  35206  ballotlemfrcn0  35232  signswn0  35259  signswch  35260  itgexpif  35305  repr0  35310  tgoldbachgtda  35360  morleylemrneab  35370  noinfepfnregs  35900  pconnconn  36163  unbdqndv2lem2  37554  knoppndvlem13  37568  qdiff  38440  sucneqond  38480  finxpreclem2  38505  finxp1o  38507  maxidln0  39171  hdmapip0  43164  fldhmf1  43332  hashscontpow1  43363  aks6d1c6lem4  43415  aks6d1c7lem1  43422  remul01  43651  3cubeslem4  43892  3cubes  43893  pellexlem6  44034  nlimsuc  44634  mnuprdlem2  45449  inaex  45473  n0p  46267  disjrnmpt2  46408  dstregt0  46503  upbdrech2  46529  xrlexaddrp  46569  infleinflem2  46587  xrralrecnnge  46606  supminfxr2  46684  absimnre  46691  xrpnf  46700  ressioosup  46772  ressiooinf  46774  fmul01lt1lem1  46801  limcperiod  46845  climxrrelem  46964  sinaover2ne0  47083  fperdvper  47134  dvdivbd  47138  itgioocnicc  47192  stirlinglem5  47293  dirker2re  47307  dirkerdenne0  47308  dirkerper  47311  dirkertrigeqlem3  47315  dirkertrigeq  47316  dirkercncflem1  47318  dirkercncflem2  47319  dirkercncflem4  47321  fourierdlem24  47346  fourierdlem25  47347  fourierdlem40  47362  fourierdlem41  47363  fourierdlem42  47364  fourierdlem44  47366  fourierdlem48  47369  fourierdlem49  47370  fourierdlem57  47378  fourierdlem58  47379  fourierdlem59  47380  fourierdlem66  47387  fourierdlem68  47389  fourierdlem74  47395  fourierdlem75  47396  fourierdlem78  47399  fourierdlem80  47401  fourierdlem81  47402  fourierdlem109  47430  elaa2lem  47448  etransclem9  47458  etransclem35  47484  etransclem38  47487  sge0tsms  47595  sge0cl  47596  sge0fodjrnlem  47631  meadjun  47677  meadjiunlem  47680  hoicvr  47763  hoidmvlelem2  47811  hoiqssbllem3  47839  sigardiv  48076  sigarcol  48079  sharhght  48080  difltmodne  48623  minusmodnep2tmod  48634  modm1p1ne  48651  prmdvdsfmtnof1lem2  48875  gpg3kgrtriexlem5  49390  inlinecirc02plem  50103  fucofvalne  50652  fullthinc  50790  euendfunc2  50867