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

Theorem necon3abid 2479
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 2448 . 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 1623    =/= wne 2446
This theorem is referenced by:  necon3bbid  2480  foconst  5462  fndmdif  5629  om00el  6574  oeoa  6595  cardsdom2  7621  mulne0b  9409  crne0  9739  expneg  11111  hashsdom  11363  gcdn0gt0  12701  pltval3  14101  mulgnegnn  14577  drngmulne0  15534  lvecvsn0  15862  domnmuln0  16039  mvrf1  16170  connsub  17147  pthaus  17332  xkohaus  17347  bndth  18456  lebnumlem1  18459  dvcobr  19295  dvcnvlem  19323  mdegle0  19463  coemulhi  19635  vieta1lem1  19690  vieta1lem2  19691  aalioulem2  19713  cosne0  19892  atandm3  20174  wilthlem2  20307  issqf  20374  mumullem2  20418  dchrptlem3  20505  lgseisenlem3  20590  nmlno0lem  21371  nmlnop0iALT  22575  atcvat2i  22967  brbtwn2  24533  colinearalg  24538  rencldnfilem  26903  qirropth  26993  bnj1542  28889  bnj1253  29047  llnexchb2  30058  cdlemb3  30795
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 2448
  Copyright terms: Public domain W3C validator