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

Theorem necon3bbid 2480
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 192 . . 3  |-  ( ph  ->  ( A  =  B  <->  ps ) )
32necon3abid 2479 . 2  |-  ( ph  ->  ( A  =/=  B  <->  -. 
ps ) )
43bicomd 192 1  |-  ( ph  ->  ( -.  ps  <->  A  =/=  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    = wceq 1623    =/= wne 2446
This theorem is referenced by:  necon3bid  2481  eldifsn  3749  reusv6OLD  4545  reusv7OLD  4546  php  7045  xmullem2  10585  seqcoll2  11402  cnpart  11725  rlimrecl  12054  prmrp  12780  4sqlem17  13008  mrieqvd  13540  mrieqv2d  13541  pltval  14094  latnlemlt  14190  latnle  14191  odnncl  14860  gexnnod  14899  sylow1lem1  14909  slwpss  14923  lssnle  14983  lspsnne1  15870  nzrunit  16018  psrridm  16149  cnsubrg  16432  cmpfi  17135  hausdiag  17339  txhaus  17341  recld2  18320  metdseq0  18358  i1f1lem  19044  aaliou2b  19721  dvloglem  19995  logf1o2  19997  lgsne0  20572  lgsqr  20585  2sqlem7  20609  ostth3  20787  norm1exi  21829  atnemeq0  22957  subfacp1lem6  23716  maxidln1  26669  smprngopr  26677  lsatnem0  29235  atncmp  29502  atncvrN  29505  cdlema2N  29981  lhpmatb  30220  lhpat3  30235  cdleme3  30426  cdleme7  30438  cdlemg27b  30885  dvh2dimatN  31630  dvh2dim  31635  dochexmidlem1  31650  dochfln0  31667
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 177  df-ne 2448
  Copyright terms: Public domain W3C validator