Theorem necon3abid 2830

Description: Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)

Hypothesis

Ref	Expression
necon3abid.1	|- ( ph -> ( A = B <-> ps ) )

Assertion

Ref	Expression
necon3abid	|- ( ph -> ( A =/= B <-> -. ps ) )

Proof of Theorem necon3abid

Step	Hyp	Ref	Expression
1		df-ne 2795	. 2 |- ( A =/= B <-> -. A = B )
2		necon3abid.1	. . 3 |- ( ph -> ( A = B <-> ps ) )
3	2	notbid 308	. 2 |- ( ph -> ( -. A = B <-> -. ps ) )
4	1, 3	syl5bb 272	1 |- ( ph -> ( A =/= B <-> -. ps ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   = wceq 1483   =/= wne 2794

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 197  df-ne 2795

This theorem is referenced by:  necon3bbid  2831  necon2abid  2836  foconst  6126  fndmdif  6321  suppsnop  7309  om00el  7656  oeoa  7677  cardsdom2  8814  mulne0b  10668  crne0  11013  expneg  12868  hashsdom  13170  prprrab  13255  gcdn0gt0  15239  cncongr2  15382  pltval3  16967  mulgnegnn  17551  drngmulne0  18769  lvecvsn0  19109  domnmuln0  19298  mvrf1  19425  connsub  21224  pthaus  21441  xkohaus  21456  bndth  22757  lebnumlem1  22760  dvcobr  23709  dvcnvlem  23739  mdegle0  23837  coemulhi  24010  vieta1lem1  24065  vieta1lem2  24066  aalioulem2  24088  cosne0  24276  atandm3  24605  wilthlem2  24795  issqf  24862  mumullem2  24906  dchrptlem3  24991  lgseisenlem3  25102  brbtwn2  25785  colinearalg  25790  vdn0conngrumgrv2  27056  vdgn1frgrv2  27160  nmlno0lem  27648  nmlnop0iALT  28854  atcvat2i  29246  divnumden2  29564  bnj1542  30927  bnj1253  31085  ptrecube  33409  poimirlem13  33422  ecinn0  34118  llnexchb2  35155  cdlemb3  35894  rencldnfilem  37384  qirropth  37473  binomcxplemfrat  38550  binomcxplemradcnv  38551  odz2prm2pw  41475