Theorem neii 2962

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

Syntax hints:  ¬ wn 3   = wceq 1563   ≠ wne 2960

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 210  df-ne 2961

This theorem is referenced by:  nesymi  3017  nemtbir  3056  snsssn  4802  nlim1  8462  nlim2  8463  2dom  9015  map2xp  9123  snnen2o  9193  ssttrcl  9672  ttrclselem2  9683  updjudhcoinrg  9907  pm54.43lem  9974  canthp1lem2  10626  ine0  11637  ind1a  12220  xrltnr  13135  pnfnlt  13144  prprrab  14500  tpf1ofv1  14524  tpf1ofv2  14525  wrdlen2i  14969  sgnnbi  15131  sgnpbi  15132  3lcm2e6woprm  16663  6lcm4e12  16664  m1dvdsndvds  16848  fnpr2ob  17602  fvprif  17605  pmatcollpw3fi1lem1  22904  sinhalfpilem  26586  coseq1  26648  2lgslem3  27526  2lgslem4  27528  ltsval2  27778  nosgnn0  27780  ltsintdifex  27783  ltsres  27784  ltssolem1  27797  nolt02o  27817  nogt01o  27818  axlowdimlem13  29213  axlowdim1  29218  umgredgnlp  29406  wwlksnext  30151  norm1exi  31511  largei  32528  rtelextdg2lem  34033  2sqr3minply  34087  2sqr3nconstr  34088  cos9thpinconstrlem2  34097  ballotlemii  34811  gonanegoal  35715  gonan0  35755  goaln0  35756  fmlasucdisj  35762  ex-sategoelelomsuc  35789  ex-sategoelel12  35790  dfrdg2  36156  dfrdg4  36314  bj-1nel0  37451  bj-pr21val  37510  finxpreclem2  37896  epnsymrel  39157  0dioph  43371  oaomoencom  43906  clsk1indlem1  44633  dirkercncflem2  46676  fourierdlem60  46738  fourierdlem61  46739  afv20defat  47824  fun2dmnopgexmpl  47876  usgrexmpl2nb0  48651  usgrexmpl2nb1  48652  usgrexmpl2nb2  48653  usgrexmpl2nb3  48654  usgrexmpl2nb4  48655  usgrexmpl2nb5  48656  itcoval1  49294  line2ylem  49382  fucofvalne  49954