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

Theorem neneqad 2676
Description: If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2619. One-way deduction form of df-ne 2603. (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 120 . 2  |-  ( A  =  B  ->  -.  ph )
32necon2ai 2651 1  |-  ( ph  ->  A  =/=  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1369    =/= wne 2601
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 2603
This theorem is referenced by:  ne0i  3638  sdomdif  7451  2pwne  7459  mapdom2  7474  canthp1lem2  8812  wrdlen2i  12538  isprm2  13763  isprm5  13790  maducoeval2  18426  alexsub  19597  ioorf  21033  dvtaylp  21815  isosctrlem1  22196  isosctrlem2  22197  chordthmlem  22207  efrlim  22343  lgsfcl2  22621  lgscllem  22622  lgsval2lem  22625  dchrisumn0  22750  tgbtwndiff  22939  tgbtwnconn1lem3  22986  ncolne1  23012  ncolne2  23013  tglineneq  23029  miriso  23051  symquadlem  23060  krippenlem  23061  midexlem  23063  ragflat3  23076  axlowdim1  23173  eupath  23570  nmcfnlbi  25424  strlem1  25622  divnumden2  26055  xrge0neqmnf  26120  xrge0npcan  26125  ornglmullt  26243  orngrmullt  26244  xrge0iifhom  26336  qqhf  26384  qqhre  26415  logccne0  26424  ballotlemi1  26854  ballotlemii  26855  ballotlemfrcn0  26881  plymulx0  26917  signswn0  26930  signswch  26931  signstfvneq0  26942  pconcon  27089  nodenselem3  27793  maxidln0  28816  pellexlem6  29146  stirlinglem5  29844  sigardiv  29868  sigarcol  29871  sharhght  29872  otsndisj  30102  hdmapip0  35456
  Copyright terms: Public domain W3C validator