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  8514  addneintr2d  8515  negne0bd  8630  negned  8634  subne0d  8646  subne0ad  8648  subneintrd  8681  subneintr2d  8683  qapne  10039  xrlttri3  10199  xaddass2  10272  seqf1oglem1  10956  sqne0  11042  fihashneq0  11233  hashnncl  11234  ccat1st1st  11409  pfxn0  11460  cjne0  11674  absne0d  11953  sqrt2irraplemnn  12957  4sqlem11  13180  ballotfilemfrcn0  13273  ringinvnz1ne0  14354  rrgsupp  14574  metn0  15479  perfectlem2  16114  lgsabs1  16158  umgrclwwlkge2  16643  neap0mkv  17119