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

Theorem necon3abid 2708
Description: Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)
Hypothesis
Ref Expression
necon3abid.1  |-  ( ph  ->  ( A  =  B  <->  ps ) )
Assertion
Ref Expression
necon3abid  |-  ( ph  ->  ( A  =/=  B  <->  -. 
ps ) )

Proof of Theorem necon3abid
StepHypRef Expression
1 df-ne 2659 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 necon3abid.1 . . 3  |-  ( ph  ->  ( A  =  B  <->  ps ) )
32notbid 294 . 2  |-  ( ph  ->  ( -.  A  =  B  <->  -.  ps )
)
41, 3syl5bb 257 1  |-  ( ph  ->  ( A  =/=  B  <->  -. 
ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    = wceq 1374    =/= wne 2657
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 2659
This theorem is referenced by:  necon3bbid  2709  necon2abid  2716  foconst  5799  fndmdif  5978  suppsnop  6907  om00el  7217  oeoa  7238  cardsdom2  8360  mulne0b  10181  crne0  10520  expneg  12132  hashsdom  12406  gcdn0gt0  14010  pltval3  15445  mulgnegnn  15947  drngmulne0  17196  lvecvsn0  17533  domnmuln0  17713  mvrf1  17847  connsub  19683  pthaus  19869  xkohaus  19884  bndth  21188  lebnumlem1  21191  dvcobr  22079  dvcnvlem  22107  mdegle0  22207  coemulhi  22380  vieta1lem1  22435  vieta1lem2  22436  aalioulem2  22458  cosne0  22645  atandm3  22932  wilthlem2  23066  issqf  23133  mumullem2  23177  dchrptlem3  23264  lgseisenlem3  23349  brbtwn2  23879  colinearalg  23884  vdn0frgrav2  24688  vdgn0frgrav2  24689  vdn1frgrav2  24690  vdgn1frgrav2  24691  nmlno0lem  25372  nmlnop0iALT  26578  atcvat2i  26970  divnumden2  27264  rencldnfilem  30347  qirropth  30437  bnj1542  32871  bnj1253  33029  llnexchb2  34542  cdlemb3  35279
  Copyright terms: Public domain W3C validator