Theorem neii 2942

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

Syntax hints:  ¬ wn 3   = wceq 1540   ≠ wne 2940

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 2941

This theorem is referenced by:  nesymi  2998  nemtbir  3038  snsssn  4841  nlim1  8527  nlim2  8528  2dom  9070  map2xp  9187  snnen2o  9273  ssttrcl  9755  ttrclselem2  9766  updjudhcoinrg  9973  pm54.43lem  10040  canthp1lem2  10693  ine0  11698  inelr  12256  xrltnr  13161  pnfnlt  13170  prprrab  14512  tpf1ofv1  14536  tpf1ofv2  14537  wrdlen2i  14981  3lcm2e6woprm  16652  6lcm4e12  16653  m1dvdsndvds  16836  fnpr2ob  17603  fvprif  17606  pmatcollpw3fi1lem1  22792  sinhalfpilem  26505  coseq1  26567  2lgslem3  27448  2lgslem4  27450  sltval2  27701  nosgnn0  27703  sltintdifex  27706  sltres  27707  sltsolem1  27720  nolt02o  27740  nogt01o  27741  axlowdimlem13  28969  axlowdim1  28974  umgredgnlp  29164  wwlksnext  29913  norm1exi  31269  largei  32286  ind1a  32844  rtelextdg2lem  33767  2sqr3minply  33791  ballotlemii  34506  sgnnbi  34548  sgnpbi  34549  gonanegoal  35357  gonan0  35397  goaln0  35398  fmlasucdisj  35404  ex-sategoelelomsuc  35431  ex-sategoelel12  35432  dfrdg2  35796  dfrdg4  35952  bj-1nel0  36955  bj-pr21val  37014  finxpreclem2  37391  epnsymrel  38563  sn-inelr  42497  0dioph  42789  oaomoencom  43330  clsk1indlem1  44058  dirkercncflem2  46119  fourierdlem60  46181  fourierdlem61  46182  afv20defat  47244  fun2dmnopgexmpl  47296  usgrexmpl2nb0  47990  usgrexmpl2nb1  47991  usgrexmpl2nb2  47992  usgrexmpl2nb3  47993  usgrexmpl2nb4  47994  usgrexmpl2nb5  47995  itcoval1  48584  line2ylem  48672  fucofvalne  49020