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

Theorem necon3abid 2635
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 2622 . 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 1369    =/= wne 2620
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 2622
This theorem is referenced by:  necon3bbid  2636  foconst  5652  fndmdif  5828  suppsnop  6725  om00el  7036  oeoa  7057  cardsdom2  8179  mulne0b  9998  crne0  10336  expneg  11894  hashsdom  12165  gcdn0gt0  13727  pltval3  15158  mulgnegnn  15658  drngmulne0  16876  lvecvsn0  17212  domnmuln0  17392  mvrf1  17520  connsub  19047  pthaus  19233  xkohaus  19248  bndth  20552  lebnumlem1  20555  dvcobr  21442  dvcnvlem  21470  mdegle0  21570  coemulhi  21743  vieta1lem1  21798  vieta1lem2  21799  aalioulem2  21821  cosne0  22008  atandm3  22295  wilthlem2  22429  issqf  22496  mumullem2  22540  dchrptlem3  22627  lgseisenlem3  22712  brbtwn2  23173  colinearalg  23178  nmlno0lem  24215  nmlnop0iALT  25421  atcvat2i  25813  divnumden2  26109  rencldnfilem  29185  qirropth  29275  vdn0frgrav2  30642  vdgn0frgrav2  30643  vdn1frgrav2  30644  vdgn1frgrav2  30645  bnj1542  31946  bnj1253  32104  llnexchb2  33609  cdlemb3  34346
  Copyright terms: Public domain W3C validator