Theorem neii 2944

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

Syntax hints:  ¬ wn 3   = wceq 1539   ≠ wne 2942

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 2943

This theorem is referenced by:  nesymi  3000  nemtbir  3039  snsssn  4769  2dom  8774  map2xp  8883  updjudhcoinrg  9622  pm54.43lem  9689  canthp1lem2  10340  ine0  11340  inelr  11893  xrltnr  12784  pnfnlt  12793  prprrab  14115  wrdlen2i  14583  3lcm2e6woprm  16248  6lcm4e12  16249  m1dvdsndvds  16427  fnpr2ob  17186  fvprif  17189  pmatcollpw3fi1lem1  21843  sinhalfpilem  25525  coseq1  25586  2lgslem3  26457  2lgslem4  26459  axlowdimlem13  27225  axlowdim1  27230  umgredgnlp  27420  wwlksnext  28159  norm1exi  29513  largei  30530  ind1a  31887  ballotlemii  32370  sgnnbi  32412  sgnpbi  32413  gonanegoal  33214  gonan0  33254  goaln0  33255  fmlasucdisj  33261  ex-sategoelelomsuc  33288  ex-sategoelel12  33289  dfrdg2  33677  ssttrcl  33701  ttrclselem2  33712  sltval2  33786  nosgnn0  33788  sltintdifex  33791  sltres  33792  sltsolem1  33805  nolt02o  33825  nogt01o  33826  dfrdg4  34180  bj-1nel0  35071  bj-pr21val  35130  finxpreclem2  35488  epnsymrel  36603  sn-inelr  40356  0dioph  40516  clsk1indlem1  41544  dirkercncflem2  43535  fourierdlem60  43597  fourierdlem61  43598  afv20defat  44611  fun2dmnopgexmpl  44663  itcoval1  45897  line2ylem  45985