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

Theorem neneqad 2637
Description: If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2583. One-way deduction form of df-ne 2569. (Contributed by David Moews, 28-Feb-2017.)
Hypothesis
Ref Expression
neneqad.1  |-  ( ph  ->  -.  A  =  B )
Assertion
Ref Expression
neneqad  |-  ( ph  ->  A  =/=  B )

Proof of Theorem neneqad
StepHypRef Expression
1 neneqad.1 . . 3  |-  ( ph  ->  -.  A  =  B )
21con2i 114 . 2  |-  ( A  =  B  ->  -.  ph )
32necon2ai 2612 1  |-  ( ph  ->  A  =/=  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1649    =/= wne 2567
This theorem is referenced by:  ne0i  3594  sdomdif  7214  2pwne  7222  mapdom2  7237  canthp1lem2  8484  isprm2  13042  isprm5  13067  alexsub  18029  ioorf  19418  dvtaylp  20239  isosctrlem1  20615  isosctrlem2  20616  chordthmlem  20626  efrlim  20761  lgsfcl2  21039  lgscllem  21040  lgsval2lem  21043  dchrisumn0  21168  eupath  21656  nmcfnlbi  23508  strlem1  23706  divnumden2  24114  xrge0neqmnf  24165  xrge0npcan  24169  xrge0iifhom  24276  qqhf  24323  qqhre  24339  logccne0  24349  ballotlemi1  24713  ballotlemii  24714  ballotlemfrcn0  24740  pconcon  24871  nodenselem3  25551  axlowdim1  25802  maxidln0  26545  pellexlem6  26787  stirlinglem5  27694  sigardiv  27718  sigarcol  27721  sharhght  27722  otsndisj  27953  hdmapip0  32401
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-ne 2569
  Copyright terms: Public domain W3C validator