Theorem necon3bid 2381

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 2341	. 2 |- ( A =/= B <-> -. A = B )
2		necon3bid.1	. . 3 |- ( ph -> ( A = B <-> C = D ) )
3	2	necon3bbid 2380	. 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 1348   =/= wne 2340

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 609  ax-in2 610

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

This theorem is referenced by:  nebidc  2420  addneintrd  8096  addneintr2d  8097  negne0bd  8212  negned  8216  subne0d  8228  subne0ad  8230  subneintrd  8263  subneintr2d  8265  qapne  9587  xrlttri3  9743  xaddass2  9816  sqne0  10530  fihashneq0  10718  hashnncl  10719  cjne0  10861  absne0d  11140  sqrt2irraplemnn  12122  metn0  13133  lgsabs1  13695