Theorem neii 2940

Description: Inference associated with df-ne 2939. (Contributed by BJ, 7-Jul-2018.)

Hypothesis

Ref	Expression
neii.1	⊢ 𝐴 ≠ 𝐵

Assertion

Ref	Expression
neii	⊢ ¬ 𝐴 = 𝐵

Proof of Theorem neii

Step	Hyp	Ref	Expression
1		neii.1	. 2 ⊢ 𝐴 ≠ 𝐵
2		df-ne 2939	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	1, 2	mpbi 230	1 ⊢ ¬ 𝐴 = 𝐵

Syntax hints:  ¬ wn 3   = wceq 1537   ≠ wne 2938

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 2939

This theorem is referenced by:  nesymi  2996  nemtbir  3036  snsssn  4846  nlim1  8526  nlim2  8527  2dom  9069  map2xp  9186  snnen2o  9271  ssttrcl  9753  ttrclselem2  9764  updjudhcoinrg  9971  pm54.43lem  10038  canthp1lem2  10691  ine0  11696  inelr  12254  xrltnr  13159  pnfnlt  13168  prprrab  14509  tpf1ofv1  14533  tpf1ofv2  14534  wrdlen2i  14978  3lcm2e6woprm  16649  6lcm4e12  16650  m1dvdsndvds  16832  fnpr2ob  17605  fvprif  17608  pmatcollpw3fi1lem1  22808  sinhalfpilem  26520  coseq1  26582  2lgslem3  27463  2lgslem4  27465  sltval2  27716  nosgnn0  27718  sltintdifex  27721  sltres  27722  sltsolem1  27735  nolt02o  27755  nogt01o  27756  axlowdimlem13  28984  axlowdim1  28989  umgredgnlp  29179  wwlksnext  29923  norm1exi  31279  largei  32296  rtelextdg2lem  33732  2sqr3minply  33753  ind1a  34000  ballotlemii  34485  sgnnbi  34527  sgnpbi  34528  gonanegoal  35337  gonan0  35377  goaln0  35378  fmlasucdisj  35384  ex-sategoelelomsuc  35411  ex-sategoelel12  35412  dfrdg2  35777  dfrdg4  35933  bj-1nel0  36937  bj-pr21val  36996  finxpreclem2  37373  epnsymrel  38544  sn-inelr  42474  0dioph  42766  oaomoencom  43307  clsk1indlem1  44035  dirkercncflem2  46060  fourierdlem60  46122  fourierdlem61  46123  afv20defat  47182  fun2dmnopgexmpl  47234  usgrexmpl2nb0  47926  usgrexmpl2nb1  47927  usgrexmpl2nb2  47928  usgrexmpl2nb3  47929  usgrexmpl2nb4  47930  usgrexmpl2nb5  47931  itcoval1  48513  line2ylem  48601