Theorem necon3bid 2401

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 2361	. 2 |- ( A =/= B <-> -. A = B )
2		necon3bid.1	. . 3 |- ( ph -> ( A = B <-> C = D ) )
3	2	necon3bbid 2400	. 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 2360

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 2361

This theorem is referenced by:  nebidc  2440  addneintrd  8163  addneintr2d  8164  negne0bd  8279  negned  8283  subne0d  8295  subne0ad  8297  subneintrd  8330  subneintr2d  8332  qapne  9657  xrlttri3  9815  xaddass2  9888  sqne0  10604  fihashneq0  10792  hashnncl  10793  cjne0  10935  absne0d  11214  sqrt2irraplemnn  12197  ringinvnz1ne0  13362  metn0  14275  lgsabs1  14837  neap0mkv  15215