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 193 . . 3  |-  ( ph  ->  ( A  =  B  <->  ps ) )
32necon3abid 2631 . 2  |-  ( ph  ->  ( A  =/=  B  <->  -. 
ps ) )
43bicomd 193 1  |-  ( ph  ->  ( -.  ps  <->  A  =/=  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    = wceq 1652    =/= wne 2598
This theorem is referenced by:  necon3bid  2633  eldifsn  3919  reusv6OLD  4726  reusv7OLD  4727  php  7283  xmullem2  10836  seqcoll2  11705  cnpart  12037  rlimrecl  12366  prmrp  13093  4sqlem17  13321  mrieqvd  13855  mrieqv2d  13856  pltval  14409  latnlemlt  14505  latnle  14506  odnncl  15175  gexnnod  15214  sylow1lem1  15224  slwpss  15238  lssnle  15298  lspsnne1  16181  nzrunit  16329  psrridm  16460  cnsubrg  16751  cmpfi  17463  hausdiag  17669  txhaus  17671  isusp  18283  recld2  18837  metdseq0  18876  i1f1lem  19573  aaliou2b  20250  dvloglem  20531  logf1o2  20533  lgsne0  21109  lgsqr  21122  2sqlem7  21146  ostth3  21324  norm1exi  22744  atnemeq0  23872  elzrhunit  24355  subfacp1lem6  24863  maxidln1  26645  smprngopr  26653  lsatnem0  29780  atncmp  30047  atncvrN  30050  cdlema2N  30526  lhpmatb  30765  lhpat3  30780  cdleme3  30971  cdleme7  30983  cdlemg27b  31430  dvh2dimatN  32175  dvh2dim  32180  dochexmidlem1  32195  dochfln0  32212
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 178  df-ne 2600
  Copyright terms: Public domain W3C validator