Theorem neqne 2954

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 22	. 2 ⊢ (¬ 𝐴 = 𝐵 → ¬ 𝐴 = 𝐵)
2	1	neqned 2953	1 ⊢ (¬ 𝐴 = 𝐵 → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2946

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 2947

This theorem is referenced by:  exmidne  2956  2f1fvneq  7297  domwdom  9643  epnsym  9678  dfac2b  10200  fin23lem14  10402  axcc2lem  10505  fiminre2  12243  cshw1  14870  xptrrel  15029  dvdsabseq  16361  ncoprmgcdne1b  16697  sgrp2rid2  18961  symg2bas  19434  symgextf  19459  odlem1  19577  gexlem1  19621  ablsimpgfind  20154  psgndiflemB  21641  cply1mul  22321  dmatmul  22524  mdetdiag  22626  mdetunilem9  22647  maducoeval2  22667  madurid  22671  chfacfisf  22881  chfacfisfcpmat  22882  plyexmo  26373  aalioulem3  26394  dvradcnv  26482  logtayllem  26719  logtayl  26720  upgriswlk  29677  lfgrwlkprop  29723  2pthnloop  29767  umgr2adedgspth  29981  umgrclwwlkge2  30023  n4cyclfrgr  30323  frgrwopreglem3  30346  frgrregorufr0  30356  domnmuln0rd  33246  elrspunsn  33422  satfv1lem  35330  bj-rest10b  37055  aks6d1c2p2  42076  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  aks6d1c6lem3  42129  aks6d1c7  42141  unitscyglem2  42153  metakunt2  42163  xppss12  42222  sn-0tie0  42415  prjspnfv01  42579  prjspner01  42580  fiiuncl  44967  disjf1  45090  fzisoeu  45215  fzdifsuc2  45225  supxrge  45253  suplesup  45254  infrpge  45266  xrlexaddrp  45267  infleinflem1  45285  infleinflem2  45286  infleinf  45287  xralrple3  45289  xrralrecnnge  45305  infxrpnf  45361  supminfxr  45379  fsumsupp0  45499  limcresiooub  45563  limcresioolb  45564  limclr  45576  climisp  45667  climxlim2lem  45766  dfxlim2v  45768  xlimliminflimsup  45783  icccncfext  45808  cncfiooiccre  45816  dvbdfbdioolem2  45850  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnxpaek  45863  dvnprodlem3  45869  itgioocnicc  45898  ovolsplit  45909  stoweidlem14  45935  stoweidlem55  45976  stoweid  45984  dirkertrigeqlem3  46021  dirkertrigeq  46022  dirkercncf  46028  fourierdlem9  46037  fourierdlem30  46058  fourierdlem31  46059  fourierdlem33  46061  fourierdlem34  46062  fourierdlem35  46063  fourierdlem42  46070  fourierdlem43  46071  fourierdlem46  46073  fourierdlem48  46075  fourierdlem49  46076  fourierdlem51  46078  fourierdlem54  46081  fourierdlem62  46089  fourierdlem64  46091  fourierdlem65  46092  fourierdlem70  46097  fourierdlem71  46098  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem79  46106  fourierdlem81  46108  fourierdlem82  46109  fourierdlem89  46116  fourierdlem91  46118  fourierdlem102  46129  fourierdlem114  46141  sqwvfoura  46149  fourierswlem  46151  fouriersw  46152  elaa2lem  46154  etransclem25  46180  etransclem28  46183  etransclem35  46190  etransclem38  46193  qndenserrnbl  46216  ioorrnopn  46226  ioorrnopnxrlem  46227  ioorrnopnxr  46228  prsal  46239  issalnnd  46266  sge0cl  46302  sge0pr  46315  sge0prle  46322  sge0isum  46348  sge0xaddlem1  46354  iundjiun  46381  meadjun  46383  ismeannd  46388  caragenfiiuncl  46436  caragenunicl  46445  isomennd  46452  hoicvr  46469  ovnssle  46482  ovn0  46487  ovnsubadd  46493  hoidmvval0b  46511  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvle  46521  ovnhoilem1  46522  ovnhoi  46524  ovnlecvr2  46531  hoiqssbl  46546  hspmbllem2  46548  hspmbl  46550  vonhoire  46593  iunhoiioo  46597  vonioo  46603  vonicc  46606  vonsn  46612  smfpimltxr  46668  smfpimgtxr  46701  smfrec  46710  fmtnoprmfac1  47439  fmtnoprmfac2  47441  lighneallem3  47481