Theorem neii 2940

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

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

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 206  df-ne 2939

This theorem is referenced by:  nesymi  2996  nemtbir  3035  snsssn  4775  nlim1  8339  nlim2  8340  2dom  8844  map2xp  8959  snnen2o  9045  ssttrcl  9501  ttrclselem2  9512  updjudhcoinrg  9719  pm54.43lem  9786  canthp1lem2  10437  ine0  11438  inelr  11991  xrltnr  12883  pnfnlt  12892  prprrab  14215  wrdlen2i  14683  3lcm2e6woprm  16348  6lcm4e12  16349  m1dvdsndvds  16527  fnpr2ob  17297  fvprif  17300  pmatcollpw3fi1lem1  21963  sinhalfpilem  25648  coseq1  25709  2lgslem3  26580  2lgslem4  26582  axlowdimlem13  27350  axlowdim1  27355  umgredgnlp  27545  wwlksnext  28286  norm1exi  29640  largei  30657  ind1a  32015  ballotlemii  32498  sgnnbi  32540  sgnpbi  32541  gonanegoal  33342  gonan0  33382  goaln0  33383  fmlasucdisj  33389  ex-sategoelelomsuc  33416  ex-sategoelel12  33417  dfrdg2  33799  sltval2  33887  nosgnn0  33889  sltintdifex  33892  sltres  33893  sltsolem1  33906  nolt02o  33926  nogt01o  33927  dfrdg4  34281  bj-1nel0  35172  bj-pr21val  35231  finxpreclem2  35589  epnsymrel  36702  sn-inelr  40458  0dioph  40623  clsk1indlem1  41679  dirkercncflem2  43680  fourierdlem60  43742  fourierdlem61  43743  afv20defat  44764  fun2dmnopgexmpl  44816  itcoval1  46049  line2ylem  46137