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

Theorem necon3abid 2700
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 2651 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 necon3abid.1 . . 3  |-  ( ph  ->  ( A  =  B  <->  ps ) )
32notbid 292 . 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 1398    =/= wne 2649
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 2651
This theorem is referenced by:  necon3bbid  2701  necon2abid  2708  foconst  5788  fndmdif  5967  suppsnop  6905  om00el  7217  oeoa  7238  cardsdom2  8360  mulne0b  10186  crne0  10524  expneg  12156  hashsdom  12432  gcdn0gt0  14244  pltval3  15796  mulgnegnn  16351  drngmulne0  17613  lvecvsn0  17950  domnmuln0  18142  mvrf1  18276  connsub  20088  pthaus  20305  xkohaus  20320  bndth  21624  lebnumlem1  21627  dvcobr  22515  dvcnvlem  22543  mdegle0  22643  coemulhi  22817  vieta1lem1  22872  vieta1lem2  22873  aalioulem2  22895  cosne0  23083  atandm3  23406  wilthlem2  23541  issqf  23608  mumullem2  23652  dchrptlem3  23739  lgseisenlem3  23824  brbtwn2  24410  colinearalg  24415  vdn0frgrav2  25225  vdgn0frgrav2  25226  vdn1frgrav2  25227  vdgn1frgrav2  25228  nmlno0lem  25906  nmlnop0iALT  27112  atcvat2i  27504  divnumden2  27843  rencldnfilem  30993  qirropth  31083  binomcxplemfrat  31497  binomcxplemradcnv  31498  bnj1542  34316  bnj1253  34474  llnexchb2  35990  cdlemb3  36729
  Copyright terms: Public domain W3C validator