Theorem necon3bid 2350

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 2310	. 2 |- ( A =/= B <-> -. A = B )
2		necon3bid.1	. . 3 |- ( ph -> ( A = B <-> C = D ) )
3	2	necon3bbid 2349	. 2 |- ( ph -> ( -. A = B <-> C =/= D ) )
4	1, 3	syl5bb 191	1 |- ( ph -> ( A =/= B <-> C =/= D ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 104   = wceq 1332   =/= wne 2309

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605

This theorem depends on definitions:  df-bi 116  df-ne 2310

This theorem is referenced by:  nebidc  2389  addneintrd  7974  addneintr2d  7975  negne0bd  8090  negned  8094  subne0d  8106  subne0ad  8108  subneintrd  8141  subneintr2d  8143  qapne  9458  xrlttri3  9613  xaddass2  9683  sqne0  10389  fihashneq0  10573  hashnncl  10574  cjne0  10712  absne0d  10991  sqrt2irraplemnn  11893  metn0  12586