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

Theorem necon3abid 2631
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 2600 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 necon3abid.1 . . 3  |-  ( ph  ->  ( A  =  B  <->  ps ) )
32notbid 286 . 2  |-  ( ph  ->  ( -.  A  =  B  <->  -.  ps )
)
41, 3syl5bb 249 1  |-  ( ph  ->  ( A  =/=  B  <->  -. 
ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    = wceq 1652    =/= wne 2598
This theorem is referenced by:  necon3bbid  2632  foconst  5656  fndmdif  5826  om00el  6811  oeoa  6832  cardsdom2  7867  mulne0b  9655  crne0  9985  expneg  11381  hashsdom  11647  gcdn0gt0  13014  pltval3  14416  mulgnegnn  14892  drngmulne0  15849  lvecvsn0  16173  domnmuln0  16350  mvrf1  16481  connsub  17476  pthaus  17662  xkohaus  17677  bndth  18975  lebnumlem1  18978  dvcobr  19824  dvcnvlem  19852  mdegle0  19992  coemulhi  20164  vieta1lem1  20219  vieta1lem2  20220  aalioulem2  20242  cosne0  20424  atandm3  20710  wilthlem2  20844  issqf  20911  mumullem2  20955  dchrptlem3  21042  lgseisenlem3  21127  nmlno0lem  22286  nmlnop0iALT  23490  atcvat2i  23882  divnumden2  24153  brbtwn2  25836  colinearalg  25841  rencldnfilem  26872  qirropth  26962  2cshwmod  28223  vdn0frgrav2  28351  vdgn0frgrav2  28352  vdn1frgrav2  28353  vdgn1frgrav2  28354  bnj1542  29165  bnj1253  29323  llnexchb2  30603  cdlemb3  31340
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 178  df-ne 2600
  Copyright terms: Public domain W3C validator