Theorem necon3bid 2441

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 2401	. 2 |- ( A =/= B <-> -. A = B )
2		necon3bid.1	. . 3 |- ( ph -> ( A = B <-> C = D ) )
3	2	necon3bbid 2440	. 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 1395   =/= wne 2400

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 617  ax-in2 618

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

This theorem is referenced by:  nebidc  2480  addneintrd  8334  addneintr2d  8335  negne0bd  8450  negned  8454  subne0d  8466  subne0ad  8468  subneintrd  8501  subneintr2d  8503  qapne  9834  xrlttri3  9993  xaddass2  10066  seqf1oglem1  10741  sqne0  10827  fihashneq0  11016  hashnncl  11017  ccat1st1st  11172  pfxn0  11220  cjne0  11419  absne0d  11698  sqrt2irraplemnn  12701  4sqlem11  12924  ringinvnz1ne0  14012  metn0  15052  perfectlem2  15674  lgsabs1  15718  neap0mkv  16437