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

Theorem necon3bbid 2493
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 2492 . 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 1632    =/= wne 2459
This theorem is referenced by:  necon3bid  2494  eldifsn  3762  reusv6OLD  4561  reusv7OLD  4562  php  7061  xmullem2  10601  seqcoll2  11418  cnpart  11741  rlimrecl  12070  prmrp  12796  4sqlem17  13024  mrieqvd  13556  mrieqv2d  13557  pltval  14110  latnlemlt  14206  latnle  14207  odnncl  14876  gexnnod  14915  sylow1lem1  14925  slwpss  14939  lssnle  14999  lspsnne1  15886  nzrunit  16034  psrridm  16165  cnsubrg  16448  cmpfi  17151  hausdiag  17355  txhaus  17357  recld2  18336  metdseq0  18374  i1f1lem  19060  aaliou2b  19737  dvloglem  20011  logf1o2  20013  lgsne0  20588  lgsqr  20601  2sqlem7  20625  ostth3  20803  norm1exi  21845  atnemeq0  22973  subfacp1lem6  23731  maxidln1  26772  smprngopr  26780  lsatnem0  29857  atncmp  30124  atncvrN  30127  cdlema2N  30603  lhpmatb  30842  lhpat3  30857  cdleme3  31048  cdleme7  31060  cdlemg27b  31507  dvh2dimatN  32252  dvh2dim  32257  dochexmidlem1  32272  dochfln0  32289
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 2461
  Copyright terms: Public domain W3C validator