Theorem necon3bid 2408

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 2368	. 2 |- ( A =/= B <-> -. A = B )
2		necon3bid.1	. . 3 |- ( ph -> ( A = B <-> C = D ) )
3	2	necon3bbid 2407	. 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 1364   =/= wne 2367

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 2368

This theorem is referenced by:  nebidc  2447  addneintrd  8216  addneintr2d  8217  negne0bd  8332  negned  8336  subne0d  8348  subne0ad  8350  subneintrd  8383  subneintr2d  8385  qapne  9715  xrlttri3  9874  xaddass2  9947  seqf1oglem1  10613  sqne0  10699  fihashneq0  10888  hashnncl  10889  cjne0  11075  absne0d  11354  sqrt2irraplemnn  12357  4sqlem11  12580  ringinvnz1ne0  13615  metn0  14624  perfectlem2  15246  lgsabs1  15290  neap0mkv  15723