Theorem neqne 2963

Description: From non-equality to inequality. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Assertion

Ref	Expression
neqne	⊢ (¬ 𝐴 = 𝐵 → 𝐴 ≠ 𝐵)

Proof of Theorem neqne

Step	Hyp	Ref	Expression
1		id 23	. 2 ⊢ (¬ 𝐴 = 𝐵 → ¬ 𝐴 = 𝐵)
2	1	neqned 2962	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:  exmidne  2965  domwdom  9568  epnsym  9610  dfac2b  10209  fin23lem14  10411  axcc2lem  10514  fiminre2  12265  cshw1  14973  xptrrel  15133  dvdsabseq  16483  ncoprmgcdne1b  16825  sgrp2rid2  19125  symg2bas  19607  symgextf  19631  odlem1  19749  gexlem1  19793  ablsimpgfind  20326  psgndiflemB  21906  cply1mul  22614  dmatmul  22812  mdetdiag  22914  mdetunilem9  22935  maducoeval2  22955  madurid  22959  chfacfisf  23172  chfacfisfcpmat  23173  plyexmo  26636  aalioulem3  26661  dvradcnv  26748  logtayllem  26987  logtayl  26988  upgriswlk  30221  lfgrwlkprop  30270  2pthnloop  30317  umgr2adedgspth  30537  umgrclwwlkge2  30582  n4cyclfrgr  30892  frgrwopreglem3  30915  frgrregorufr0  30925  domnmuln0rd  33838  elrspunsn  33979  drnglring  34024  dflringlem3  34028  dflring4  34030  satfv1lem  36127  bj-rest10b  38010  aks6d1c2p2  43170  sticksstones10  43206  sticksstones12a  43208  sticksstones12  43209  aks6d1c6lem3  43223  aks6d1c7  43235  unitscyglem2  43247  xppss12  43284  sn-0tie0  43516  fiiuncl  46082  disjf1  46198  fzisoeu  46316  fzdifsuc2  46326  supxrge  46350  suplesup  46351  infrpge  46363  xrlexaddrp  46364  infleinflem1  46381  infleinflem2  46382  infleinf  46383  xralrple3  46385  xrralrecnnge  46401  infxrpnf  46456  supminfxr  46474  fsumsupp0  46590  limcresiooub  46652  limcresioolb  46653  limclr  46665  climisp  46756  climxlim2lem  46855  dfxlim2v  46857  xlimliminflimsup  46872  icccncfext  46897  cncfiooiccre  46905  dvbdfbdioolem2  46939  ioodvbdlimc1lem2  46942  ioodvbdlimc2lem  46944  dvnxpaek  46952  dvnprodlem3  46958  itgioocnicc  46987  ovolsplit  46998  stoweidlem14  47024  stoweidlem55  47065  stoweid  47073  dirkertrigeqlem3  47110  dirkertrigeq  47111  dirkercncf  47117  fourierdlem9  47126  fourierdlem30  47147  fourierdlem31  47148  fourierdlem33  47150  fourierdlem34  47151  fourierdlem35  47152  fourierdlem42  47159  fourierdlem43  47160  fourierdlem46  47162  fourierdlem48  47164  fourierdlem49  47165  fourierdlem51  47167  fourierdlem54  47170  fourierdlem62  47178  fourierdlem64  47180  fourierdlem65  47181  fourierdlem70  47186  fourierdlem71  47187  fourierdlem73  47189  fourierdlem74  47190  fourierdlem75  47191  fourierdlem76  47192  fourierdlem79  47195  fourierdlem81  47197  fourierdlem82  47198  fourierdlem89  47205  fourierdlem91  47207  fourierdlem102  47218  fourierdlem114  47230  sqwvfoura  47238  fourierswlem  47240  fouriersw  47241  elaa2lem  47243  etransclem25  47269  etransclem28  47272  etransclem35  47279  etransclem38  47282  qndenserrnbl  47305  ioorrnopn  47315  ioorrnopnxrlem  47316  ioorrnopnxr  47317  prsal  47328  issalnnd  47355  sge0cl  47391  sge0pr  47404  sge0prle  47411  sge0isum  47437  sge0xaddlem1  47443  iundjiun  47470  meadjun  47472  ismeannd  47477  caragenfiiuncl  47525  caragenunicl  47534  isomennd  47541  hoicvr  47558  ovnssle  47571  ovn0  47576  ovnsubadd  47582  hoidmvval0b  47600  hoidmvlelem2  47606  hoidmvlelem3  47607  hoidmvle  47610  ovnhoilem1  47611  ovnhoi  47613  ovnlecvr2  47620  hoiqssbl  47635  hspmbllem2  47637  hspmbl  47639  vonhoire  47682  iunhoiioo  47686  vonioo  47692  vonicc  47695  vonsn  47701  smfpimltxr  47757  smfpimgtxr  47790  smfrec  47799  fmtnoprmfac1  48650  fmtnoprmfac2  48652  lighneallem3  48692  pgn4cyclex  49224