Theorem neii 2948

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

Syntax hints:  ¬ wn 3   = wceq 1537   ≠ wne 2946

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 2947

This theorem is referenced by:  nesymi  3004  nemtbir  3044  snsssn  4866  nlim1  8545  nlim2  8546  2dom  9095  map2xp  9213  snnen2o  9300  ssttrcl  9784  ttrclselem2  9795  updjudhcoinrg  10002  pm54.43lem  10069  canthp1lem2  10722  ine0  11725  inelr  12283  xrltnr  13182  pnfnlt  13191  prprrab  14522  tpf1ofv1  14546  tpf1ofv2  14547  wrdlen2i  14991  3lcm2e6woprm  16662  6lcm4e12  16663  m1dvdsndvds  16845  fnpr2ob  17618  fvprif  17621  pmatcollpw3fi1lem1  22813  sinhalfpilem  26523  coseq1  26585  2lgslem3  27466  2lgslem4  27468  sltval2  27719  nosgnn0  27721  sltintdifex  27724  sltres  27725  sltsolem1  27738  nolt02o  27758  nogt01o  27759  axlowdimlem13  28987  axlowdim1  28992  umgredgnlp  29182  wwlksnext  29926  norm1exi  31282  largei  32299  rtelextdg2lem  33717  2sqr3minply  33738  ind1a  33983  ballotlemii  34468  sgnnbi  34510  sgnpbi  34511  gonanegoal  35320  gonan0  35360  goaln0  35361  fmlasucdisj  35367  ex-sategoelelomsuc  35394  ex-sategoelel12  35395  dfrdg2  35759  dfrdg4  35915  bj-1nel0  36920  bj-pr21val  36979  finxpreclem2  37356  epnsymrel  38518  sn-inelr  42443  0dioph  42734  oaomoencom  43279  clsk1indlem1  44007  dirkercncflem2  46025  fourierdlem60  46087  fourierdlem61  46088  afv20defat  47147  fun2dmnopgexmpl  47199  usgrexmpl2nb0  47846  usgrexmpl2nb1  47847  usgrexmpl2nb2  47848  usgrexmpl2nb3  47849  usgrexmpl2nb4  47850  usgrexmpl2nb5  47851  itcoval1  48397  line2ylem  48485