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

Theorem necon3bbid 2632
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 2631 . 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 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:  necon3bid  2633  eldifsn  3988  reusv6OLD  4491  reusv7OLD  4492  php  7483  xmullem2  11215  seqcoll2  12200  cnpart  12712  rlimrecl  13041  prmrp  13769  4sqlem17  14004  mrieqvd  14558  mrieqv2d  14559  pltval  15112  latnlemlt  15236  latnle  15237  odnncl  16027  gexnnod  16066  sylow1lem1  16076  slwpss  16090  lssnle  16150  lspsnne1  17119  nzrunit  17269  psrridm  17409  psrridmOLD  17410  cnsubrg  17716  mdet1  18249  cmpfi  18852  hausdiag  19059  txhaus  19061  isusp  19677  recld2  20232  metdseq0  20271  i1f1lem  21008  aaliou2b  21691  dvloglem  21977  logf1o2  21979  lgsne0  22556  lgsqr  22569  2sqlem7  22593  ostth3  22771  tgelrnln  22906  tghilbert1_1  22913  norm1exi  24475  atnemeq0  25603  ordtconlem1  26207  elzrhunit  26261  sgnneg  26770  subfacp1lem6  26920  maxidln1  28685  smprngopr  28693  lsatnem0  32260  atncmp  32527  atncvrN  32530  cdlema2N  33006  lhpmatb  33245  lhpat3  33260  cdleme3  33451  cdleme7  33463  cdlemg27b  33910  dvh2dimatN  34655  dvh2dim  34660  dochexmidlem1  34675  dochfln0  34692
  Copyright terms: Public domain W3C validator