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

Theorem necon3bbid 2714
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 2713 . 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 1379    =/= wne 2662
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 2664
This theorem is referenced by:  necon1abid  2715  necon3bid  2725  eldifsn  4152  reusv6OLD  4658  reusv7OLD  4659  php  7698  xmullem2  11453  seqcoll2  12475  cnpart  13032  rlimrecl  13362  prmrp  14097  4sqlem17  14334  mrieqvd  14889  mrieqv2d  14890  pltval  15443  latnlemlt  15567  latnle  15568  odnncl  16365  gexnnod  16404  sylow1lem1  16414  slwpss  16428  lssnle  16488  lspsnne1  17546  nzrunit  17696  psrridm  17829  psrridmOLD  17830  cnsubrg  18246  cmpfi  19674  hausdiag  19881  txhaus  19883  isusp  20499  recld2  21054  metdseq0  21093  i1f1lem  21831  aaliou2b  22471  dvloglem  22757  logf1o2  22759  lgsne0  23336  lgsqr  23349  2sqlem7  23373  ostth3  23551  tglngne  23665  tgelrnln  23724  tghilbert1_1  23731  norm1exi  25844  atnemeq0  26972  ordtconlem1  27542  elzrhunit  27596  qtophaus  27637  sgnneg  28119  subfacp1lem6  28269  maxidln1  30044  smprngopr  30052  lsatnem0  33842  atncmp  34109  atncvrN  34112  cdlema2N  34588  lhpmatb  34827  lhpat3  34842  cdleme3  35033  cdleme7  35045  cdlemg27b  35492  dvh2dimatN  36237  dvh2dim  36242  dochexmidlem1  36257  dochfln0  36274
  Copyright terms: Public domain W3C validator