Theorem necon3bid 2417

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 2377	. 2 |- ( A =/= B <-> -. A = B )
2		necon3bid.1	. . 3 |- ( ph -> ( A = B <-> C = D ) )
3	2	necon3bbid 2416	. 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 1373   =/= wne 2376

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 615  ax-in2 616

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

This theorem is referenced by:  nebidc  2456  addneintrd  8262  addneintr2d  8263  negne0bd  8378  negned  8382  subne0d  8394  subne0ad  8396  subneintrd  8429  subneintr2d  8431  qapne  9762  xrlttri3  9921  xaddass2  9994  seqf1oglem1  10666  sqne0  10752  fihashneq0  10941  hashnncl  10942  ccat1st1st  11096  pfxn0  11142  cjne0  11252  absne0d  11531  sqrt2irraplemnn  12534  4sqlem11  12757  ringinvnz1ne0  13844  metn0  14883  perfectlem2  15505  lgsabs1  15549  neap0mkv  16045