Theorem necon3bid 2347

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 2307	. 2 |- ( A =/= B <-> -. A = B )
2		necon3bid.1	. . 3 |- ( ph -> ( A = B <-> C = D ) )
3	2	necon3bbid 2346	. 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 1331   =/= wne 2306

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 603  ax-in2 604

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

This theorem is referenced by:  nebidc  2386  addneintrd  7943  addneintr2d  7944  negne0bd  8059  negned  8063  subne0d  8075  subne0ad  8077  subneintrd  8110  subneintr2d  8112  qapne  9424  xrlttri3  9576  xaddass2  9646  sqne0  10351  fihashneq0  10534  hashnncl  10535  cjne0  10673  absne0d  10952  sqrt2irraplemnn  11846  metn0  12536