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  8345  addneintr2d  8346  negne0bd  8461  negned  8465  subne0d  8477  subne0ad  8479  subneintrd  8512  subneintr2d  8514  qapne  9846  xrlttri3  10005  xaddass2  10078  seqf1oglem1  10753  sqne0  10839  fihashneq0  11028  hashnncl  11029  ccat1st1st  11188  pfxn0  11236  cjne0  11435  absne0d  11714  sqrt2irraplemnn  12717  4sqlem11  12940  ringinvnz1ne0  14028  metn0  15068  perfectlem2  15690  lgsabs1  15734  umgrclwwlkge2  16145  neap0mkv  16525