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

Theorem necon3bbid 2647
Description: Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.)
Hypothesis
Ref Expression
necon3bbid.1  |-  ( ph  ->  ( ps  <->  A  =  B ) )
Assertion
Ref Expression
necon3bbid  |-  ( ph  ->  ( -.  ps  <->  A  =/=  B ) )

Proof of Theorem necon3bbid
StepHypRef Expression
1 necon3bbid.1 . . . 4  |-  ( ph  ->  ( ps  <->  A  =  B ) )
21bicomd 201 . . 3  |-  ( ph  ->  ( A  =  B  <->  ps ) )
32necon3abid 2646 . 2  |-  ( ph  ->  ( A  =/=  B  <->  -. 
ps ) )
43bicomd 201 1  |-  ( ph  ->  ( -.  ps  <->  A  =/=  B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    = wceq 1369    =/= wne 2611
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 2613
This theorem is referenced by:  necon3bid  2648  eldifsn  4005  reusv6OLD  4508  reusv7OLD  4509  php  7500  xmullem2  11233  seqcoll2  12222  cnpart  12734  rlimrecl  13063  prmrp  13792  4sqlem17  14027  mrieqvd  14581  mrieqv2d  14582  pltval  15135  latnlemlt  15259  latnle  15260  odnncl  16053  gexnnod  16092  sylow1lem1  16102  slwpss  16116  lssnle  16176  lspsnne1  17203  nzrunit  17353  psrridm  17481  psrridmOLD  17482  cnsubrg  17878  mdet1  18413  cmpfi  19016  hausdiag  19223  txhaus  19225  isusp  19841  recld2  20396  metdseq0  20435  i1f1lem  21172  aaliou2b  21812  dvloglem  22098  logf1o2  22100  lgsne0  22677  lgsqr  22690  2sqlem7  22714  ostth3  22892  tglngne  22989  tgelrnln  23041  tghilbert1_1  23048  norm1exi  24658  atnemeq0  25786  ordtconlem1  26359  elzrhunit  26413  sgnneg  26928  subfacp1lem6  27078  maxidln1  28849  smprngopr  28857  lsatnem0  32695  atncmp  32962  atncvrN  32965  cdlema2N  33441  lhpmatb  33680  lhpat3  33695  cdleme3  33886  cdleme7  33898  cdlemg27b  34345  dvh2dimatN  35090  dvh2dim  35095  dochexmidlem1  35110  dochfln0  35127
  Copyright terms: Public domain W3C validator