Theorem neii 2935

Description: Inference associated with df-ne 2934. (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 2934	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	1, 2	mpbi 230	1 ⊢ ¬ 𝐴 = 𝐵

Syntax hints:  ¬ wn 3   = wceq 1540   ≠ 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:  nesymi  2990  nemtbir  3029  snsssn  4822  nlim1  8506  nlim2  8507  2dom  9049  map2xp  9166  snnen2o  9250  ssttrcl  9734  ttrclselem2  9745  updjudhcoinrg  9952  pm54.43lem  10019  canthp1lem2  10672  ine0  11677  inelr  12235  xrltnr  13140  pnfnlt  13149  prprrab  14496  tpf1ofv1  14520  tpf1ofv2  14521  wrdlen2i  14966  3lcm2e6woprm  16639  6lcm4e12  16640  m1dvdsndvds  16823  fnpr2ob  17577  fvprif  17580  pmatcollpw3fi1lem1  22729  sinhalfpilem  26429  coseq1  26491  2lgslem3  27372  2lgslem4  27374  sltval2  27625  nosgnn0  27627  sltintdifex  27630  sltres  27631  sltsolem1  27644  nolt02o  27664  nogt01o  27665  axlowdimlem13  28938  axlowdim1  28943  umgredgnlp  29131  wwlksnext  29880  norm1exi  31236  largei  32253  sgnnbi  32822  sgnpbi  32823  ind1a  32841  rtelextdg2lem  33765  2sqr3minply  33819  2sqr3nconstr  33820  ballotlemii  34541  gonanegoal  35379  gonan0  35419  goaln0  35420  fmlasucdisj  35426  ex-sategoelelomsuc  35453  ex-sategoelel12  35454  dfrdg2  35818  dfrdg4  35974  bj-1nel0  36977  bj-pr21val  37036  finxpreclem2  37413  epnsymrel  38585  sn-inelr  42477  0dioph  42768  oaomoencom  43308  clsk1indlem1  44036  dirkercncflem2  46100  fourierdlem60  46162  fourierdlem61  46163  afv20defat  47228  fun2dmnopgexmpl  47280  usgrexmpl2nb0  48002  usgrexmpl2nb1  48003  usgrexmpl2nb2  48004  usgrexmpl2nb3  48005  usgrexmpl2nb4  48006  usgrexmpl2nb5  48007  itcoval1  48610  line2ylem  48698  fucofvalne  49203