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  4785  nlim1  8417  nlim2  8418  2dom  8970  map2xp  9078  snnen2o  9148  ssttrcl  9627  ttrclselem2  9638  updjudhcoinrg  9848  pm54.43lem  9915  canthp1lem2  10567  ine0  11576  ind1a  12161  xrltnr  13061  pnfnlt  13070  prprrab  14426  tpf1ofv1  14450  tpf1ofv2  14451  wrdlen2i  14895  3lcm2e6woprm  16575  6lcm4e12  16576  m1dvdsndvds  16760  fnpr2ob  17513  fvprif  17516  pmatcollpw3fi1lem1  22761  sinhalfpilem  26440  coseq1  26502  2lgslem3  27381  2lgslem4  27383  ltsval2  27634  nosgnn0  27636  ltsintdifex  27639  ltsres  27640  ltssolem1  27653  nolt02o  27673  nogt01o  27674  axlowdimlem13  29037  axlowdim1  29042  umgredgnlp  29230  wwlksnext  29976  norm1exi  31336  largei  32353  sgnnbi  32926  sgnpbi  32927  rtelextdg2lem  33886  2sqr3minply  33940  2sqr3nconstr  33941  cos9thpinconstrlem2  33950  ballotlemii  34664  gonanegoal  35550  gonan0  35590  goaln0  35591  fmlasucdisj  35597  ex-sategoelelomsuc  35624  ex-sategoelel12  35625  dfrdg2  35991  dfrdg4  36149  bj-1nel0  37277  bj-pr21val  37336  finxpreclem2  37720  epnsymrel  38981  0dioph  43224  oaomoencom  43763  clsk1indlem1  44490  dirkercncflem2  46550  fourierdlem60  46612  fourierdlem61  46613  afv20defat  47692  fun2dmnopgexmpl  47744  usgrexmpl2nb0  48519  usgrexmpl2nb1  48520  usgrexmpl2nb2  48521  usgrexmpl2nb3  48522  usgrexmpl2nb4  48523  usgrexmpl2nb5  48524  itcoval1  49151  line2ylem  49239  fucofvalne  49812