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

Theorem necon3abid 2600
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 2569 . 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 1649    =/= wne 2567
This theorem is referenced by:  necon3bbid  2601  foconst  5623  fndmdif  5793  om00el  6778  oeoa  6799  cardsdom2  7831  mulne0b  9619  crne0  9949  expneg  11344  hashsdom  11610  gcdn0gt0  12977  pltval3  14379  mulgnegnn  14855  drngmulne0  15812  lvecvsn0  16136  domnmuln0  16313  mvrf1  16444  connsub  17437  pthaus  17623  xkohaus  17638  bndth  18936  lebnumlem1  18939  dvcobr  19785  dvcnvlem  19813  mdegle0  19953  coemulhi  20125  vieta1lem1  20180  vieta1lem2  20181  aalioulem2  20203  cosne0  20385  atandm3  20671  wilthlem2  20805  issqf  20872  mumullem2  20916  dchrptlem3  21003  lgseisenlem3  21088  nmlno0lem  22247  nmlnop0iALT  23451  atcvat2i  23843  divnumden2  24114  brbtwn2  25748  colinearalg  25753  rencldnfilem  26771  qirropth  26861  vdn0frgrav2  28128  vdgn0frgrav2  28129  vdn1frgrav2  28130  vdgn1frgrav2  28131  bnj1542  28934  bnj1253  29092  llnexchb2  30351  cdlemb3  31088
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 2569
  Copyright terms: Public domain W3C validator