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

Theorem neneqad 2652
Description: If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2651. One-way deduction form of df-ne 2646. (Contributed by David Moews, 28-Feb-2017.) Revised to shorten necon3bi 2677. (Revised by Wolf Lammen, 22-Nov-2019.)
Hypothesis
Ref Expression
neneqad.1  |-  ( ph  ->  -.  A  =  B )
Assertion
Ref Expression
neneqad  |-  ( ph  ->  A  =/=  B )

Proof of Theorem neneqad
StepHypRef Expression
1 neneqad.1 . 2  |-  ( ph  ->  -.  A  =  B )
2 df-ne 2646 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2sylibr 212 1  |-  ( ph  ->  A  =/=  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1370    =/= wne 2644
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 2646
This theorem is referenced by:  necon3bi  2677  necon2ai  2683  necon3i  2688  ne0i  3743  sdomdif  7561  2pwne  7569  mapdom2  7584  canthp1lem2  8923  wrdlen2i  12650  isprm2  13875  isprm5  13902  maducoeval2  18564  alexsub  19735  ioorf  21171  dvtaylp  21953  isosctrlem1  22334  isosctrlem2  22335  chordthmlem  22345  efrlim  22481  lgsfcl2  22759  lgscllem  22760  lgsval2lem  22763  dchrisumn0  22888  tgbtwnne  23063  tgbtwndiff  23079  tgbtwnconn1lem3  23128  ncolne1  23155  ncolne2  23156  tglineneq  23173  tglowdim2ln  23181  miriso  23201  symquadlem  23211  krippenlem  23212  midexlem  23214  ragflat3  23228  ragperp  23238  footex  23239  colperplem2  23243  colperplem3  23244  mideulem  23246  axlowdim1  23342  eupath  23739  nmcfnlbi  25593  strlem1  25791  divnumden2  26223  xrge0neqmnf  26288  xrge0npcan  26293  ornglmullt  26411  orngrmullt  26412  xrge0iifhom  26503  qqhf  26551  qqhre  26582  logccne0  26591  ballotlemi1  27021  ballotlemii  27022  ballotlemfrcn0  27048  plymulx0  27084  signswn0  27097  signswch  27098  signstfvneq0  27109  pconcon  27256  nodenselem3  27960  maxidln0  28985  pellexlem6  29315  stirlinglem5  30013  sigardiv  30037  sigarcol  30040  sharhght  30041  otsndisj  30271  hdmapip0  35871
  Copyright terms: Public domain W3C validator