Theorem neqne 2942

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 2941	1 ⊢ (¬ 𝐴 = 𝐵 → 𝐴 ≠ 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2934

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 210  df-ne 2935

This theorem is referenced by:  exmidne  2944  2f1fvneq  7023  domwdom  9104  epnsym  9138  dfac2b  9623  fin23lem14  9826  axcc2lem  9929  fiminre2  11659  cshw1  14266  xptrrel  14422  dvdsabseq  15751  ncoprmgcdne1b  16084  sgrp2rid2  18200  symg2bas  18632  symgextf  18656  odlem1  18774  gexlem1  18815  ablsimpgfind  19344  psgndiflemB  20409  cply1mul  21062  dmatmul  21241  mdetdiag  21343  mdetunilem9  21364  maducoeval2  21384  madurid  21388  chfacfisf  21598  chfacfisfcpmat  21599  plyexmo  25053  aalioulem3  25074  dvradcnv  25160  logtayllem  25394  logtayl  25395  upgriswlk  27574  lfgrwlkprop  27621  2pthnloop  27664  umgr2adedgspth  27878  umgrclwwlkge2  27920  n4cyclfrgr  28220  frgrwopreglem3  28243  frgrregorufr0  28253  satfv1lem  32887  bj-rest10b  34870  metakunt2  39706  xppss12  39770  sn-0tie0  39982  prjspnfv01  40022  prjspner01  40023  fiiuncl  42135  disjf1  42242  fzisoeu  42361  fzdifsuc2  42371  supxrge  42399  suplesup  42400  infrpge  42412  xrlexaddrp  42413  infleinflem1  42431  infleinflem2  42432  infleinf  42433  xralrple3  42435  xrralrecnnge  42452  infxrpnf  42509  supminfxr  42528  fsumsupp0  42645  limcresiooub  42709  limcresioolb  42710  limclr  42722  climisp  42813  climxlim2lem  42912  dfxlim2v  42914  xlimliminflimsup  42929  icccncfext  42954  cncfiooiccre  42962  dvbdfbdioolem2  42996  ioodvbdlimc1lem2  42999  ioodvbdlimc2lem  43001  dvnxpaek  43009  dvnprodlem3  43015  itgioocnicc  43044  ovolsplit  43055  stoweidlem14  43081  stoweidlem55  43122  stoweid  43130  dirkertrigeqlem3  43167  dirkertrigeq  43168  dirkercncf  43174  fourierdlem9  43183  fourierdlem30  43204  fourierdlem31  43205  fourierdlem33  43207  fourierdlem34  43208  fourierdlem35  43209  fourierdlem42  43216  fourierdlem43  43217  fourierdlem46  43219  fourierdlem48  43221  fourierdlem49  43222  fourierdlem51  43224  fourierdlem54  43227  fourierdlem62  43235  fourierdlem64  43237  fourierdlem65  43238  fourierdlem70  43243  fourierdlem71  43244  fourierdlem73  43246  fourierdlem74  43247  fourierdlem75  43248  fourierdlem76  43249  fourierdlem79  43252  fourierdlem81  43254  fourierdlem82  43255  fourierdlem89  43262  fourierdlem91  43264  fourierdlem102  43275  fourierdlem114  43287  sqwvfoura  43295  fourierswlem  43297  fouriersw  43298  elaa2lem  43300  etransclem25  43326  etransclem28  43329  etransclem35  43336  etransclem38  43339  qndenserrnbl  43362  ioorrnopn  43372  ioorrnopnxrlem  43373  ioorrnopnxr  43374  prsal  43385  issalnnd  43410  sge0cl  43445  sge0pr  43458  sge0prle  43465  sge0isum  43491  sge0xaddlem1  43497  iundjiun  43524  meadjun  43526  ismeannd  43531  caragenfiiuncl  43579  caragenunicl  43588  isomennd  43595  hoicvr  43612  ovnssle  43625  ovn0  43630  ovnsubadd  43636  hoidmvval0b  43654  hoidmvlelem2  43660  hoidmvlelem3  43661  hoidmvle  43664  ovnhoilem1  43665  ovnhoi  43667  ovnlecvr2  43674  hoiqssbl  43689  hspmbllem2  43691  hspmbl  43693  vonhoire  43736  iunhoiioo  43740  vonioo  43746  vonicc  43749  vonsn  43755  smfpimltxr  43806  smfpimgtxr  43838  smfrec  43846  fmtnoprmfac1  44535  fmtnoprmfac2  44537  lighneallem3  44577