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

Theorem necon3abid 2636
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 2603 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 necon3abid.1 . . 3  |-  ( ph  ->  ( A  =  B  <->  ps ) )
32notbid 287 . 2  |-  ( ph  ->  ( -.  A  =  B  <->  -.  ps )
)
41, 3syl5bb 250 1  |-  ( ph  ->  ( A  =/=  B  <->  -. 
ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    = wceq 1653    =/= wne 2601
This theorem is referenced by:  necon3bbid  2637  foconst  5667  fndmdif  5837  om00el  6822  oeoa  6843  cardsdom2  7880  mulne0b  9668  crne0  9998  expneg  11394  hashsdom  11660  gcdn0gt0  13027  pltval3  14429  mulgnegnn  14905  drngmulne0  15862  lvecvsn0  16186  domnmuln0  16363  mvrf1  16494  connsub  17489  pthaus  17675  xkohaus  17690  bndth  18988  lebnumlem1  18991  dvcobr  19837  dvcnvlem  19865  mdegle0  20005  coemulhi  20177  vieta1lem1  20232  vieta1lem2  20233  aalioulem2  20255  cosne0  20437  atandm3  20723  wilthlem2  20857  issqf  20924  mumullem2  20968  dchrptlem3  21055  lgseisenlem3  21140  nmlno0lem  22299  nmlnop0iALT  23503  atcvat2i  23895  divnumden2  24166  brbtwn2  25849  colinearalg  25854  rencldnfilem  26895  qirropth  26985  2cshwmod  28291  vdn0frgrav2  28488  vdgn0frgrav2  28489  vdn1frgrav2  28490  vdgn1frgrav2  28491  bnj1542  29302  bnj1253  29460  llnexchb2  30740  cdlemb3  31477
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 179  df-ne 2603
  Copyright terms: Public domain W3C validator