MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  neii Structured version   Unicode version

Theorem neii 2659
Description: Inference associated with df-ne 2657. (Contributed by BJ, 7-Jul-2018.)
Hypothesis
Ref Expression
neii.1  |-  A  =/= 
B
Assertion
Ref Expression
neii  |-  -.  A  =  B

Proof of Theorem neii
StepHypRef Expression
1 neii.1 . 2  |-  A  =/= 
B
2 df-ne 2657 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2mpbi 208 1  |-  -.  A  =  B
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1374    =/= wne 2655
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 185  df-ne 2657
This theorem is referenced by:  nesymi  2733  nemtbir  2788  snsssn  4188  2dom  7578  map2xp  7677  pm54.43lem  8369  canthp1lem2  9020  ine0  9981  inelr  10515  xrltnr  11319  pnfnlt  11326  wrdlen2i  12834  m1dvdsndvds  14173  xpsfrnel2  14809  pmatcollpw3fi1lem1  19047  sinhalfpilem  22582  coseq1  22641  usgraedgprv  24038  wlkntrllem3  24225  4cycl4dv  24329  wwlknext  24386  sgnnbi  28110  sgnpbi  28111  usgedgnlp  31812  bj-1nel0  33466  bj-pr21val  33527
  Copyright terms: Public domain W3C validator