Theorem neii 2957

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

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2956

This theorem is used by:  nesymi  3012  nemtbir  3051  snsssn  4795  nlim1  8500  nlim2  8501  2dom  9061  map2xp  9169  snnen2o  9239  ssttrcl  9719  ttrclselem2  9730  updjudhcoinrg  10017  pm54.43lem  10084  canthp1lem2  10741  ine0  11754  ind1a  12334  xrltnr  13251  pnfnlt  13260  prprrab  14621  tpf1ofv1  14645  tpf1ofv2  14646  wrdlen2i  15098  sgnnbi  15262  sgnpbi  15263  3lcm2e6woprm  16795  6lcm4e12  16796  m1dvdsndvds  16981  fnpr2ob  17735  fvprif  17738  pmatcollpw3fi1lem1  23109  sinhalfpilem  26797  coseq1  26858  2lgslem3  27736  2lgslem4  27738  ltsval2  28018  nosgnn0  28020  ltsintdifex  28023  ltsres  28024  ltssolem1  28037  nolt02o  28057  nogt01o  28058  axlowdimlem13  29537  axlowdim1  29542  umgredgnlp  29730  wwlksnext  30487  norm1exi  31857  largei  32874  rtelextdg2lem  34404  2sqr3minply  34458  2sqr3nconstr  34459  cos9thpinconstrlem2  34468  ballotlemii  35182  gonanegoal  36203  gonan0  36243  goaln0  36244  fmlasucdisj  36250  ex-sategoelelomsuc  36277  ex-sategoelel12  36278  dfrdg2  36649  dfrdg4  36807  bj-1nel0  37959  bj-pr21val  38018  finxpreclem2  38406  epnsymrel  39671  0dioph  43882  oaomoencom  44412  clsk1indlem1  45138  dirkercncflem2  47207  fourierdlem60  47269  fourierdlem61  47270  goldratmolem4  48028  afv20defat  48395  fun2dmnopgexmpl  48447  usgrexmpl2nb0  49222  usgrexmpl2nb1  49223  usgrexmpl2nb2  49224  usgrexmpl2nb3  49225  usgrexmpl2nb4  49226  usgrexmpl2nb5  49227  itcoval1  49868  line2ylem  49956  fucofvalne  50540  parhomeqor2  50851  par2hom  50872