Theorem neii 2934

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

Syntax hints:  ¬ wn 3   = wceq 1542   ≠ wne 2932

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 2933

This theorem is referenced by:  nesymi  2989  nemtbir  3028  snsssn  4784  nlim1  8424  nlim2  8425  2dom  8977  map2xp  9085  snnen2o  9155  ssttrcl  9636  ttrclselem2  9647  updjudhcoinrg  9857  pm54.43lem  9924  canthp1lem2  10576  ine0  11585  ind1a  12170  xrltnr  13070  pnfnlt  13079  prprrab  14435  tpf1ofv1  14459  tpf1ofv2  14460  wrdlen2i  14904  3lcm2e6woprm  16584  6lcm4e12  16585  m1dvdsndvds  16769  fnpr2ob  17522  fvprif  17525  pmatcollpw3fi1lem1  22751  sinhalfpilem  26427  coseq1  26489  2lgslem3  27367  2lgslem4  27369  ltsval2  27620  nosgnn0  27622  ltsintdifex  27625  ltsres  27626  ltssolem1  27639  nolt02o  27659  nogt01o  27660  axlowdimlem13  29023  axlowdim1  29028  umgredgnlp  29216  wwlksnext  29961  norm1exi  31321  largei  32338  sgnnbi  32911  sgnpbi  32912  rtelextdg2lem  33870  2sqr3minply  33924  2sqr3nconstr  33925  cos9thpinconstrlem2  33934  ballotlemii  34648  gonanegoal  35534  gonan0  35574  goaln0  35575  fmlasucdisj  35581  ex-sategoelelomsuc  35608  ex-sategoelel12  35609  dfrdg2  35975  dfrdg4  36133  bj-1nel0  37261  bj-pr21val  37320  finxpreclem2  37706  epnsymrel  38967  0dioph  43210  oaomoencom  43745  clsk1indlem1  44472  dirkercncflem2  46532  fourierdlem60  46594  fourierdlem61  46595  afv20defat  47680  fun2dmnopgexmpl  47732  usgrexmpl2nb0  48507  usgrexmpl2nb1  48508  usgrexmpl2nb2  48509  usgrexmpl2nb3  48510  usgrexmpl2nb4  48511  usgrexmpl2nb5  48512  itcoval1  49139  line2ylem  49227  fucofvalne  49800