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  5666  fndmdif  5836  om00el  6821  oeoa  6842  cardsdom2  7877  mulne0b  9665  crne0  9995  expneg  11391  hashsdom  11657  gcdn0gt0  13024  pltval3  14426  mulgnegnn  14902  drngmulne0  15859  lvecvsn0  16183  domnmuln0  16360  mvrf1  16491  connsub  17486  pthaus  17672  xkohaus  17687  bndth  18985  lebnumlem1  18988  dvcobr  19834  dvcnvlem  19862  mdegle0  20002  coemulhi  20174  vieta1lem1  20229  vieta1lem2  20230  aalioulem2  20252  cosne0  20434  atandm3  20720  wilthlem2  20854  issqf  20921  mumullem2  20965  dchrptlem3  21052  lgseisenlem3  21137  nmlno0lem  22296  nmlnop0iALT  23500  atcvat2i  23892  divnumden2  24163  brbtwn2  25846  colinearalg  25851  rencldnfilem  26883  qirropth  26973  2cshwmod  28279  vdn0frgrav2  28476  vdgn0frgrav2  28477  vdn1frgrav2  28478  vdgn1frgrav2  28479  bnj1542  29290  bnj1253  29448  llnexchb2  30728  cdlemb3  31465
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 179  df-ne 2603
  Copyright terms: Public domain W3C validator