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 2598 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 necon3abid.1 . . 3  |-  ( ph  ->  ( A  =  B  <->  ps ) )
32notbid 294 . 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 1362    =/= wne 2596
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 2598
This theorem is referenced by:  necon3bbid  2632  foconst  5619  fndmdif  5795  suppsnop  6693  om00el  7003  oeoa  7024  cardsdom2  8146  mulne0b  9964  crne0  10302  expneg  11856  hashsdom  12127  gcdn0gt0  13688  pltval3  15119  mulgnegnn  15616  drngmulne0  16777  lvecvsn0  17111  domnmuln0  17291  mvrf1  17431  connsub  18866  pthaus  19052  xkohaus  19067  bndth  20371  lebnumlem1  20374  dvcobr  21261  dvcnvlem  21289  mdegle0  21432  coemulhi  21605  vieta1lem1  21660  vieta1lem2  21661  aalioulem2  21683  cosne0  21870  atandm3  22157  wilthlem2  22291  issqf  22358  mumullem2  22402  dchrptlem3  22489  lgseisenlem3  22574  brbtwn2  22973  colinearalg  22978  nmlno0lem  24015  nmlnop0iALT  25221  atcvat2i  25613  divnumden2  25909  rencldnfilem  29001  qirropth  29091  vdn0frgrav2  30459  vdgn0frgrav2  30460  vdn1frgrav2  30461  vdgn1frgrav2  30462  bnj1542  31549  bnj1253  31707  llnexchb2  33083  cdlemb3  33820
  Copyright terms: Public domain W3C validator