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

Theorem necon3bbid 2701
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 2700 . 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 1398    =/= wne 2649
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 2651
This theorem is referenced by:  necon1abid  2702  necon3bid  2712  eldifsn  4141  reusv6OLD  4648  reusv7OLD  4649  php  7694  xmullem2  11460  seqcoll2  12497  cnpart  13155  rlimrecl  13485  prmrp  14326  4sqlem17  14563  mrieqvd  15127  mrieqv2d  15128  pltval  15789  latnlemlt  15913  latnle  15914  odnncl  16768  gexnnod  16807  sylow1lem1  16817  slwpss  16831  lssnle  16891  lspsnne1  17958  nzrunit  18110  psrridm  18253  psrridmOLD  18254  cnsubrg  18673  cmpfi  20075  hausdiag  20312  txhaus  20314  isusp  20930  recld2  21485  metdseq0  21524  i1f1lem  22262  aaliou2b  22903  dvloglem  23197  logf1o2  23199  lgsne0  23806  lgsqr  23819  2sqlem7  23843  ostth3  24021  tglngne  24138  tgelrnln  24211  norm1exi  26366  atnemeq0  27494  opeldifid  27670  qtophaus  28074  ordtconlem1  28141  elzrhunit  28194  sgnneg  28743  subfacp1lem6  28893  maxidln1  30681  smprngopr  30689  lsatnem0  35167  atncmp  35434  atncvrN  35437  cdlema2N  35913  lhpmatb  36152  lhpat3  36167  cdleme3  36359  cdleme7  36371  cdlemg27b  36819  dvh2dimatN  37564  dvh2dim  37569  dochexmidlem1  37584  dochfln0  37601
  Copyright terms: Public domain W3C validator