Theorem neii 2963

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

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ≠ wne 2961

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2962

This theorem is used by:  nesymi  3018  nemtbir  3057  snsssn  4811  nlim1  8483  nlim2  8484  2dom  9037  map2xp  9145  snnen2o  9215  ssttrcl  9694  ttrclselem2  9705  updjudhcoinrg  9938  pm54.43lem  10005  canthp1lem2  10656  ine0  11667  ind1a  12247  xrltnr  13162  pnfnlt  13171  prprrab  14530  tpf1ofv1  14554  tpf1ofv2  14555  wrdlen2i  15005  sgnnbi  15167  sgnpbi  15168  3lcm2e6woprm  16698  6lcm4e12  16699  m1dvdsndvds  16883  fnpr2ob  17637  fvprif  17640  pmatcollpw3fi1lem1  22980  sinhalfpilem  26665  coseq1  26727  2lgslem3  27605  2lgslem4  27607  ltsval2  27857  nosgnn0  27859  ltsintdifex  27862  ltsres  27863  ltssolem1  27876  nolt02o  27896  nogt01o  27897  axlowdimlem13  29341  axlowdim1  29346  umgredgnlp  29534  wwlksnext  30279  norm1exi  31639  largei  32656  rtelextdg2lem  34147  2sqr3minply  34201  2sqr3nconstr  34202  cos9thpinconstrlem2  34211  ballotlemii  34925  gonanegoal  35864  gonan0  35904  goaln0  35905  fmlasucdisj  35911  ex-sategoelelomsuc  35938  ex-sategoelel12  35939  dfrdg2  36305  dfrdg4  36463  bj-1nel0  37630  bj-pr21val  37689  finxpreclem2  38076  epnsymrel  39335  0dioph  43549  oaomoencom  44084  clsk1indlem1  44811  dirkercncflem2  46858  fourierdlem60  46920  fourierdlem61  46921  afv20defat  48009  fun2dmnopgexmpl  48061  usgrexmpl2nb0  48836  usgrexmpl2nb1  48837  usgrexmpl2nb2  48838  usgrexmpl2nb3  48839  usgrexmpl2nb4  48840  usgrexmpl2nb5  48841  itcoval1  49483  line2ylem  49571  fucofvalne  50143