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

Theorem neneqad 2674
Description: If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2617. One-way deduction form of df-ne 2601. (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 2649 1  |-  ( ph  ->  A  =/=  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1652    =/= wne 2599
This theorem is referenced by:  ne0i  3634  sdomdif  7255  2pwne  7263  mapdom2  7278  canthp1lem2  8528  isprm2  13087  isprm5  13112  alexsub  18076  ioorf  19465  dvtaylp  20286  isosctrlem1  20662  isosctrlem2  20663  chordthmlem  20673  efrlim  20808  lgsfcl2  21086  lgscllem  21087  lgsval2lem  21090  dchrisumn0  21215  eupath  21703  nmcfnlbi  23555  strlem1  23753  divnumden2  24161  xrge0neqmnf  24212  xrge0npcan  24216  xrge0iifhom  24323  qqhf  24370  qqhre  24386  logccne0  24396  ballotlemi1  24760  ballotlemii  24761  ballotlemfrcn0  24787  pconcon  24918  nodenselem3  25638  axlowdim1  25898  maxidln0  26655  pellexlem6  26897  stirlinglem5  27803  sigardiv  27827  sigarcol  27830  sharhght  27831  otsndisj  28065  hdmapip0  32716
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 2601
  Copyright terms: Public domain W3C validator