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

Theorem necon3abid 2492
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 2461 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 necon3abid.1 . . 3  |-  ( ph  ->  ( A  =  B  <->  ps ) )
32notbid 285 . 2  |-  ( ph  ->  ( -.  A  =  B  <->  -.  ps )
)
41, 3syl5bb 248 1  |-  ( ph  ->  ( A  =/=  B  <->  -. 
ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    = wceq 1632    =/= wne 2459
This theorem is referenced by:  necon3bbid  2493  foconst  5478  fndmdif  5645  om00el  6590  oeoa  6611  cardsdom2  7637  mulne0b  9425  crne0  9755  expneg  11127  hashsdom  11379  gcdn0gt0  12717  pltval3  14117  mulgnegnn  14593  drngmulne0  15550  lvecvsn0  15878  domnmuln0  16055  mvrf1  16186  connsub  17163  pthaus  17348  xkohaus  17363  bndth  18472  lebnumlem1  18475  dvcobr  19311  dvcnvlem  19339  mdegle0  19479  coemulhi  19651  vieta1lem1  19706  vieta1lem2  19707  aalioulem2  19729  cosne0  19908  atandm3  20190  wilthlem2  20323  issqf  20390  mumullem2  20434  dchrptlem3  20521  lgseisenlem3  20606  nmlno0lem  21387  nmlnop0iALT  22591  atcvat2i  22983  brbtwn2  24605  colinearalg  24610  rencldnfilem  27006  qirropth  27096  bnj1542  29205  bnj1253  29363  llnexchb2  30680  cdlemb3  31417
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 177  df-ne 2461
  Copyright terms: Public domain W3C validator