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 1542   ≠ 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  4799  nlim1  8426  nlim2  8427  2dom  8979  map2xp  9087  snnen2o  9157  ssttrcl  9636  ttrclselem2  9647  updjudhcoinrg  9857  pm54.43lem  9924  canthp1lem2  10576  ine0  11584  xrltnr  13045  pnfnlt  13054  prprrab  14408  tpf1ofv1  14432  tpf1ofv2  14433  wrdlen2i  14877  3lcm2e6woprm  16554  6lcm4e12  16555  m1dvdsndvds  16738  fnpr2ob  17491  fvprif  17494  pmatcollpw3fi1lem1  22742  sinhalfpilem  26440  coseq1  26502  2lgslem3  27383  2lgslem4  27385  ltsval2  27636  nosgnn0  27638  ltsintdifex  27641  ltsres  27642  ltssolem1  27655  nolt02o  27675  nogt01o  27676  axlowdimlem13  29039  axlowdim1  29044  umgredgnlp  29232  wwlksnext  29978  norm1exi  31337  largei  32354  sgnnbi  32929  sgnpbi  32930  ind1a  32948  rtelextdg2lem  33903  2sqr3minply  33957  2sqr3nconstr  33958  cos9thpinconstrlem2  33967  ballotlemii  34681  gonanegoal  35565  gonan0  35605  goaln0  35606  fmlasucdisj  35612  ex-sategoelelomsuc  35639  ex-sategoelel12  35640  dfrdg2  36006  dfrdg4  36164  bj-1nel0  37196  bj-pr21val  37255  finxpreclem2  37639  epnsymrel  38891  0dioph  43129  oaomoencom  43668  clsk1indlem1  44395  dirkercncflem2  46456  fourierdlem60  46518  fourierdlem61  46519  afv20defat  47586  fun2dmnopgexmpl  47638  usgrexmpl2nb0  48385  usgrexmpl2nb1  48386  usgrexmpl2nb2  48387  usgrexmpl2nb3  48388  usgrexmpl2nb4  48389  usgrexmpl2nb5  48390  itcoval1  49017  line2ylem  49105  fucofvalne  49678