Theorem necon3bid 2461

Description: Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypothesis

Ref	Expression
necon3bid.1	|- ( ph -> ( A = B <-> C = D ) )

Assertion

Ref	Expression
necon3bid	|- ( ph -> ( A =/= B <-> C =/= D ) )

Proof of Theorem necon3bid

Step	Hyp	Ref	Expression
1		df-ne 2421	. 2 |- ( A =/= B <-> -. A = B )
2		necon3bid.1	. . 3 |- ( ph -> ( A = B <-> C = D ) )
3	2	necon3bbid 2460	. 2 |- ( ph -> ( -. A = B <-> C =/= D ) )
4	1, 3	bitrid 192	1 |- ( ph -> ( A =/= B <-> C =/= D ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   <-> wb 105   = wceq 1402   =/= wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624

This proof depends on definitions:  df-bi 117  df-ne 2421

This theorem is used by:  nebidc  2500  suppval1  6479  addneintrd  8516  addneintr2d  8517  negne0bd  8632  negned  8636  subne0d  8648  subne0ad  8650  subneintrd  8683  subneintr2d  8685  qapne  10049  xrlttri3  10210  xaddass2  10283  seqf1oglem1  10971  sqne0  11057  fihashneq0  11249  hashnncl  11250  ccat1st1st  11425  pfxn0  11476  cjne0  11690  absne0d  11970  sqrt2irraplemnn  12978  4sqlem11  13203  ballotfilemfrcn0  13325  ringinvnz1ne0  14438  rrgsupp  14658  metn0  15570  perfectlem2  16261  lgsabs1  16324  umgrclwwlkge2  16809  neap0mkv  17286