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  8428  nlim2  8429  2dom  8981  map2xp  9089  snnen2o  9159  ssttrcl  9638  ttrclselem2  9649  updjudhcoinrg  9859  pm54.43lem  9926  canthp1lem2  10578  ine0  11586  xrltnr  13047  pnfnlt  13056  prprrab  14410  tpf1ofv1  14434  tpf1ofv2  14435  wrdlen2i  14879  3lcm2e6woprm  16556  6lcm4e12  16557  m1dvdsndvds  16740  fnpr2ob  17493  fvprif  17496  pmatcollpw3fi1lem1  22747  sinhalfpilem  26445  coseq1  26507  2lgslem3  27388  2lgslem4  27390  ltsval2  27641  nosgnn0  27643  ltsintdifex  27646  ltsres  27647  ltssolem1  27660  nolt02o  27680  nogt01o  27681  axlowdimlem13  29045  axlowdim1  29050  umgredgnlp  29238  wwlksnext  29984  norm1exi  31344  largei  32361  sgnnbi  32936  sgnpbi  32937  ind1a  32955  rtelextdg2lem  33910  2sqr3minply  33964  2sqr3nconstr  33965  cos9thpinconstrlem2  33974  ballotlemii  34688  gonanegoal  35574  gonan0  35614  goaln0  35615  fmlasucdisj  35621  ex-sategoelelomsuc  35648  ex-sategoelel12  35649  dfrdg2  36015  dfrdg4  36173  bj-1nel0  37229  bj-pr21val  37288  finxpreclem2  37672  epnsymrel  38926  0dioph  43164  oaomoencom  43703  clsk1indlem1  44430  dirkercncflem2  46491  fourierdlem60  46553  fourierdlem61  46554  afv20defat  47621  fun2dmnopgexmpl  47673  usgrexmpl2nb0  48420  usgrexmpl2nb1  48421  usgrexmpl2nb2  48422  usgrexmpl2nb3  48423  usgrexmpl2nb4  48424  usgrexmpl2nb5  48425  itcoval1  49052  line2ylem  49140  fucofvalne  49713