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

Theorem necon3bbid 2637
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 194 . . 3  |-  ( ph  ->  ( A  =  B  <->  ps ) )
32necon3abid 2636 . 2  |-  ( ph  ->  ( A  =/=  B  <->  -. 
ps ) )
43bicomd 194 1  |-  ( ph  ->  ( -.  ps  <->  A  =/=  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 178    = wceq 1653    =/= wne 2601
This theorem is referenced by:  necon3bid  2638  eldifsn  3929  reusv6OLD  4737  reusv7OLD  4738  php  7294  xmullem2  10849  seqcoll2  11718  cnpart  12050  rlimrecl  12379  prmrp  13106  4sqlem17  13334  mrieqvd  13868  mrieqv2d  13869  pltval  14422  latnlemlt  14518  latnle  14519  odnncl  15188  gexnnod  15227  sylow1lem1  15237  slwpss  15251  lssnle  15311  lspsnne1  16194  nzrunit  16342  psrridm  16473  cnsubrg  16764  cmpfi  17476  hausdiag  17682  txhaus  17684  isusp  18296  recld2  18850  metdseq0  18889  i1f1lem  19584  aaliou2b  20263  dvloglem  20544  logf1o2  20546  lgsne0  21122  lgsqr  21135  2sqlem7  21159  ostth3  21337  norm1exi  22757  atnemeq0  23885  elzrhunit  24368  subfacp1lem6  24876  maxidln1  26668  smprngopr  26676  lsatnem0  29917  atncmp  30184  atncvrN  30187  cdlema2N  30663  lhpmatb  30902  lhpat3  30917  cdleme3  31108  cdleme7  31120  cdlemg27b  31567  dvh2dimatN  32312  dvh2dim  32317  dochexmidlem1  32332  dochfln0  32349
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 179  df-ne 2603
  Copyright terms: Public domain W3C validator