Theorem neqned 2962

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

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

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 2956

This theorem is used by:  neqne  2963  necon3bi  2981  necon2ai  2984  necon3i  2987  mteqand  3046  nelne1  3052  nelne2  3053  ne0i  4286  rexn0  4451  nelpr2  4613  nelpr1  4614  otsndisj  5491  rnmptn0  6245  enpr2d  9076  sdomdif  9144  2pwne  9152  mapdom2  9167  dif1enlem  9175  infn0  9294  scotteld  9947  canthp1lem2  10738  nnneneg  12373  flltnz  13951  hashpss  14554  wrdlen2i  15093  s3sndisj  15120  isprm2  16857  isprm5  16883  nnoddn2prmb  16991  chnind  18795  chnccat  18800  hashfinmndnn  18941  sgrp2nmndlem5  19128  fincygsubgodd  20328  prmgrpsimpgd  20330  ornglmullt  21126  orngrmullt  21127  pidlnz  21528  drngidl  21539  rhmpreimaprmidl  21635  qsidomlem1  21636  qsnzr  21639  psdmul  22487  alexsub  24364  ioorf  25894  dvmptdiv  26294  plyn0mulidp  26602  dvtaylp  26697  cos02pilt1  26854  logccne0  26906  isosctrlem1  27146  isosctrlem2  27147  chordthmlem  27160  efrlim  27297  lgsfcl2  27630  lgscllem  27631  lgsval2lem  27634  2sqn0  27761  2sqmod  27763  dchrisumn0  27848  flt4ALT  27992  noseponlem  28021  nosupbnd1lem3  28067  nosupbnd1lem4  28068  nosupbnd1lem5  28069  nosupbnd2lem1  28072  noinfbnd1lem3  28082  noinfbnd1lem4  28083  noinfbnd1lem5  28084  noetainflem4  28097  cutbdaybnd2lim  28183  bdayfinbndlem1  28853  z12bdaylem1  28856  tgbtwnne  28953  tgbtwndiff  28969  tgbtwnconn1lem3  29037  legov3  29061  legso  29062  ncolne1  29093  tglineneq  29113  tglowdim2ln  29120  mirne  29139  miriso  29142  mirhl  29151  mirbtwnhl  29152  symquadlem  29161  krippenlem  29162  midexlem  29164  symquadprlnglem  29165  ragflat3  29181  ragperp  29192  footexALT  29193  footexlem2  29195  colperpexlem2  29207  colperpexlem3  29208  mideulem2  29210  oppne3  29219  outpasch  29233  hlpasch  29234  plngrotlem1  29265  lmieu  29289  lmicom  29293  tgaaddcpbllem1  29349  tgaaddcpbllem2  29350  angmgmaddeu1  29379  angmgmaddov2lem  29387  prlngmolem1  29430  prlngmo2  29434  prlngplngtr  29437  prlnginn0  29438  prlngmid2  29439  symquadprlng  29440  quadcgrprlng  29444  axlowdim1  29537  wlkp1lem5  30256  wlkp1lem6  30257  eulerpathpr  30841  nmcfnlbi  32654  strlem1  32852  tgextancd  33068  tgextalem1inag  33070  tgextamirnhl  33072  unidifsnne  33174  fsuppcurry1  33358  fsuppcurry2  33359  divnumden2  33449  xrge0npcan  33623  tocyccntz  33747  elrgspnlem4  33848  fracfld  33912  drngidlhash  34025  mxidlirredi  34038  mxidlirred  34039  ssmxidl  34041  krull  34045  krullndrng  34047  qsdrng  34063  dflringlem  34068  rprmasso2  34100  rprmirred  34105  pidufd  34117  1arithufdlem3  34120  mplmulmvr  34213  esplyind  34249  vietadeg1  34252  exsslsb  34271  constrextdg2lem  34422  constrext2chnlem  34424  2sqr3nconstr  34455  cos9thpinconstrlem2  34464  zarclsint  34546  zarclssn  34547  xrge0iifhom  34611  qqhf  34660  qqhre  34694  esumrnmpt2  34742  carsgclctunlem2  34993  ballotlemi1  35177  ballotlemii  35178  ballotlemfrcn0  35204  signswn0  35231  signswch  35232  itgexpif  35277  repr0  35282  tgoldbachgtda  35332  morleylemrneab  35342  noinfepfnregs  35842  pconnconn  36038  unbdqndv2lem2  37418  knoppndvlem13  37432  qdiff  38291  sucneqond  38331  finxpreclem2  38356  finxp1o  38358  maxidln0  39022  hdmapip0  43015  fldhmf1  43183  hashscontpow1  43214  aks6d1c6lem4  43266  aks6d1c7lem1  43273  remul01  43501  3cubeslem4  43742  3cubes  43743  pellexlem6  43884  nlimsuc  44485  mnuprdlem2  45300  inaex  45324  n0p  46105  disjrnmpt2  46246  dstregt0  46341  upbdrech2  46367  xrlexaddrp  46407  infleinflem2  46425  xrralrecnnge  46444  supminfxr2  46522  absimnre  46529  xrpnf  46538  ressioosup  46610  ressiooinf  46612  fmul01lt1lem1  46639  limcperiod  46683  climxrrelem  46802  sinaover2ne0  46921  fperdvper  46972  dvdivbd  46976  itgioocnicc  47030  stirlinglem5  47131  dirker2re  47145  dirkerdenne0  47146  dirkerper  47149  dirkertrigeqlem3  47153  dirkertrigeq  47154  dirkercncflem1  47156  dirkercncflem2  47157  dirkercncflem4  47159  fourierdlem24  47184  fourierdlem25  47185  fourierdlem40  47200  fourierdlem41  47201  fourierdlem42  47202  fourierdlem44  47204  fourierdlem48  47207  fourierdlem49  47208  fourierdlem57  47216  fourierdlem58  47217  fourierdlem59  47218  fourierdlem66  47225  fourierdlem68  47227  fourierdlem74  47233  fourierdlem75  47234  fourierdlem78  47237  fourierdlem80  47239  fourierdlem81  47240  fourierdlem109  47268  elaa2lem  47286  etransclem9  47296  etransclem35  47322  etransclem38  47325  sge0tsms  47433  sge0cl  47434  sge0fodjrnlem  47469  meadjun  47515  meadjiunlem  47518  hoicvr  47601  hoidmvlelem2  47649  hoiqssbllem3  47677  sigardiv  47914  sigarcol  47917  sharhght  47918  difltmodne  48461  minusmodnep2tmod  48472  modm1p1ne  48489  prmdvdsfmtnof1lem2  48713  gpg3kgrtriexlem5  49228  fucofvalne  50476  fullthinc  50601  euendfunc2  50678