Theorem neii 2937

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

Syntax hints:  ¬ wn 3   = wceq 1547   ≠ wne 2935

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 208  df-ne 2936

This theorem is referenced by:  nesymi  2992  nemtbir  3031  snsssn  4779  nlim1  8421  nlim2  8422  2dom  8974  map2xp  9082  snnen2o  9152  ssttrcl  9634  ttrclselem2  9645  updjudhcoinrg  9855  pm54.43lem  9922  canthp1lem2  10574  ine0  11583  ind1a  12168  xrltnr  13068  pnfnlt  13077  prprrab  14433  tpf1ofv1  14457  tpf1ofv2  14458  wrdlen2i  14902  3lcm2e6woprm  16582  6lcm4e12  16583  m1dvdsndvds  16767  fnpr2ob  17520  fvprif  17523  pmatcollpw3fi1lem1  22776  sinhalfpilem  26452  coseq1  26514  2lgslem3  27392  2lgslem4  27394  ltsval2  27645  nosgnn0  27647  ltsintdifex  27650  ltsres  27651  ltssolem1  27664  nolt02o  27684  nogt01o  27685  axlowdimlem13  29048  axlowdim1  29053  umgredgnlp  29241  wwlksnext  29986  norm1exi  31346  largei  32363  sgnnbi  32937  sgnpbi  32938  rtelextdg2lem  33917  2sqr3minply  33971  2sqr3nconstr  33972  cos9thpinconstrlem2  33981  ballotlemii  34695  gonanegoal  35587  gonan0  35627  goaln0  35628  fmlasucdisj  35634  ex-sategoelelomsuc  35661  ex-sategoelel12  35662  dfrdg2  36028  dfrdg4  36186  bj-1nel0  37314  bj-pr21val  37373  finxpreclem2  37759  epnsymrel  39020  0dioph  43234  oaomoencom  43769  clsk1indlem1  44496  dirkercncflem2  46554  fourierdlem60  46616  fourierdlem61  46617  afv20defat  47702  fun2dmnopgexmpl  47754  usgrexmpl2nb0  48529  usgrexmpl2nb1  48530  usgrexmpl2nb2  48531  usgrexmpl2nb3  48532  usgrexmpl2nb4  48533  usgrexmpl2nb5  48534  itcoval1  49161  line2ylem  49249  fucofvalne  49822