Theorem neii 2958

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

Syntax hints:  ¬ wn 3   = wceq 1559   ≠ wne 2956

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 209  df-ne 2957

This theorem is referenced by:  nesymi  3013  nemtbir  3052  snsssn  4798  nlim1  8453  nlim2  8454  2dom  9007  map2xp  9115  snnen2o  9185  ssttrcl  9667  ttrclselem2  9678  updjudhcoinrg  9888  pm54.43lem  9955  canthp1lem2  10608  ine0  11619  ind1a  12203  xrltnr  13118  pnfnlt  13127  prprrab  14483  tpf1ofv1  14507  tpf1ofv2  14508  wrdlen2i  14952  3lcm2e6woprm  16632  6lcm4e12  16633  m1dvdsndvds  16817  fnpr2ob  17571  fvprif  17574  pmatcollpw3fi1lem1  22826  sinhalfpilem  26505  coseq1  26567  2lgslem3  27445  2lgslem4  27447  ltsval2  27697  nosgnn0  27699  ltsintdifex  27702  ltsres  27703  ltssolem1  27716  nolt02o  27736  nogt01o  27737  axlowdimlem13  29101  axlowdim1  29106  umgredgnlp  29294  wwlksnext  30039  norm1exi  31399  largei  32416  sgnnbi  32990  sgnpbi  32991  rtelextdg2lem  33984  2sqr3minply  34038  2sqr3nconstr  34039  cos9thpinconstrlem2  34048  ballotlemii  34762  gonanegoal  35666  gonan0  35706  goaln0  35707  fmlasucdisj  35713  ex-sategoelelomsuc  35740  ex-sategoelel12  35741  dfrdg2  36107  dfrdg4  36265  bj-1nel0  37403  bj-pr21val  37462  finxpreclem2  37848  epnsymrel  39109  0dioph  43323  oaomoencom  43858  clsk1indlem1  44585  dirkercncflem2  46642  fourierdlem60  46704  fourierdlem61  46705  afv20defat  47790  fun2dmnopgexmpl  47842  usgrexmpl2nb0  48617  usgrexmpl2nb1  48618  usgrexmpl2nb2  48619  usgrexmpl2nb3  48620  usgrexmpl2nb4  48621  usgrexmpl2nb5  48622  itcoval1  49249  line2ylem  49337  fucofvalne  49910