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  4294  rexn0  4450  nelpr2  4611  nelpr1  4612  otsndisj  5468  rnmptn0  6203  enpr2d  8989  sdomdif  9057  2pwne  9065  mapdom2  9080  dif1enlem  9088  infn0  9206  canthp1lem2  10568  nnneneg  12184  flltnz  13735  wrdlen2i  14869  s3sndisj  14894  isprm2  16613  isprm5  16638  nnoddn2prmb  16745  chnind  18548  chnccat  18553  hashfinmndnn  18680  sgrp2nmndlem5  18858  fincygsubgodd  20047  prmgrpsimpgd  20049  ornglmullt  20806  orngrmullt  20807  psdmul  22113  alexsub  23993  ioorf  25534  dvmptdiv  25938  dvtaylp  26338  cos02pilt1  26495  logccne0  26547  isosctrlem1  26788  isosctrlem2  26789  chordthmlem  26802  efrlim  26939  efrlimOLD  26940  lgsfcl2  27274  lgscllem  27275  lgsval2lem  27278  2sqn0  27405  2sqmod  27407  dchrisumn0  27492  noseponlem  27636  nosupbnd1lem3  27682  nosupbnd1lem4  27683  nosupbnd1lem5  27684  nosupbnd2lem1  27687  noinfbnd1lem3  27697  noinfbnd1lem4  27698  noinfbnd1lem5  27699  noetainflem4  27712  scutbdaybnd2lim  27795  bdayfinbndlem1  28446  zs12bdaylem1  28449  tgbtwnne  28545  tgbtwndiff  28561  tgbtwnconn1lem3  28629  legov3  28653  legso  28654  ncolne1  28680  tglineneq  28699  tglowdim2ln  28706  mirne  28722  miriso  28725  mirhl  28734  mirbtwnhl  28735  symquadlem  28744  krippenlem  28745  midexlem  28747  ragflat3  28761  ragperp  28772  footexALT  28773  footexlem2  28775  colperpexlem2  28786  colperpexlem3  28787  mideulem2  28789  oppne3  28798  outpasch  28810  hlpasch  28811  lmieu  28839  lmicom  28843  axlowdim1  29015  wlkp1lem5  29732  wlkp1lem6  29733  eulerpathpr  30298  nmcfnlbi  32110  strlem1  32308  unidifsnne  32593  fsuppcurry1  32784  fsuppcurry2  32785  hashpss  32870  divnumden2  32877  xrge0npcan  33083  tocyccntz  33207  elrgspnlem4  33308  fracfld  33371  pidlnz  33438  drngidl  33495  drngidlhash  33496  rhmpreimaprmidl  33513  qsidomlem1  33514  qsnzr  33517  mxidlirredi  33533  mxidlirred  33534  ssmxidl  33536  krull  33541  krullndrng  33543  qsdrng  33559  rprmasso2  33588  rprmirred  33593  pidufd  33605  1arithufdlem3  33608  mplmulmvr  33685  esplyind  33712  vietadeg1  33715  exsslsb  33734  constrextdg2lem  33886  constrext2chnlem  33888  2sqr3nconstr  33919  cos9thpinconstrlem2  33928  zarclsint  34010  zarclssn  34011  xrge0iifhom  34075  qqhf  34124  qqhre  34158  esumrnmpt2  34206  carsgclctunlem2  34457  ballotlemi1  34641  ballotlemii  34642  ballotlemfrcn0  34668  plymulx0  34685  signswn0  34698  signswch  34699  itgexpif  34744  repr0  34749  tgoldbachgtda  34799  noinfepfnregs  35269  pconnconn  35406  unbdqndv2lem2  36685  knoppndvlem13  36699  sucneqond  37541  finxpreclem2  37566  finxp1o  37568  maxidln0  38217  hdmapip0  42212  fldhmf1  42381  hashscontpow1  42412  aks6d1c6lem4  42464  aks6d1c7lem1  42471  remul01  42698  3cubeslem4  42967  3cubes  42968  pellexlem6  43112  nlimsuc  43718  scotteld  44523  mnuprdlem2  44550  inaex  44574  n0p  45326  disjrnmpt2  45468  dstregt0  45566  upbdrech2  45592  xrlexaddrp  45633  infleinflem2  45651  xrralrecnnge  45670  supminfxr2  45749  absimnre  45756  xrpnf  45765  ressioosup  45837  ressiooinf  45839  fmul01lt1lem1  45866  limcperiod  45910  climxrrelem  46029  sinaover2ne0  46148  fperdvper  46199  dvdivbd  46203  itgioocnicc  46257  stirlinglem5  46358  dirker2re  46372  dirkerdenne0  46373  dirkerper  46376  dirkertrigeqlem3  46380  dirkertrigeq  46381  dirkercncflem1  46383  dirkercncflem2  46384  dirkercncflem4  46386  fourierdlem24  46411  fourierdlem25  46412  fourierdlem40  46427  fourierdlem41  46428  fourierdlem42  46429  fourierdlem44  46431  fourierdlem48  46434  fourierdlem49  46435  fourierdlem57  46443  fourierdlem58  46444  fourierdlem59  46445  fourierdlem66  46452  fourierdlem68  46454  fourierdlem74  46460  fourierdlem75  46461  fourierdlem78  46464  fourierdlem80  46466  fourierdlem81  46467  fourierdlem109  46495  elaa2lem  46513  etransclem9  46523  etransclem35  46549  etransclem38  46552  sge0tsms  46660  sge0cl  46661  sge0fodjrnlem  46696  meadjun  46742  meadjiunlem  46745  hoicvr  46828  hoidmvlelem2  46876  hoiqssbllem3  46904  sigardiv  47141  sigarcol  47144  sharhght  47145  chnsubseq  47160  difltmodne  47624  minusmodnep2tmod  47635  modm1p1ne  47652  prmdvdsfmtnof1lem2  47867  gpg3kgrtriexlem5  48369  fucofvalne  49606  fullthinc  49731  euendfunc2  49808