Theorem necon3bid 2444

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 2404	. 2 |- ( A =/= B <-> -. A = B )
2		necon3bid.1	. . 3 |- ( ph -> ( A = B <-> C = D ) )
3	2	necon3bbid 2443	. 2 |- ( ph -> ( -. A = B <-> C =/= D ) )
4	1, 3	bitrid 192	1 |- ( ph -> ( A =/= B <-> C =/= D ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 105   = wceq 1398   =/= wne 2403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620

This theorem depends on definitions:  df-bi 117  df-ne 2404

This theorem is referenced by:  nebidc  2483  suppval1  6417  addneintrd  8426  addneintr2d  8427  negne0bd  8542  negned  8546  subne0d  8558  subne0ad  8560  subneintrd  8593  subneintr2d  8595  qapne  9934  xrlttri3  10093  xaddass2  10166  seqf1oglem1  10844  sqne0  10930  fihashneq0  11119  hashnncl  11120  ccat1st1st  11284  pfxn0  11335  cjne0  11548  absne0d  11827  sqrt2irraplemnn  12831  4sqlem11  13054  ringinvnz1ne0  14143  rrgsupp  14361  metn0  15189  perfectlem2  15814  lgsabs1  15858  umgrclwwlkge2  16343  neap0mkv  16802