Theorem necon3bid 2405

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 2365	. 2 |- ( A =/= B <-> -. A = B )
2		necon3bid.1	. . 3 |- ( ph -> ( A = B <-> C = D ) )
3	2	necon3bbid 2404	. 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 2364

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 2365

This theorem is referenced by:  nebidc  2444  addneintrd  8207  addneintr2d  8208  negne0bd  8323  negned  8327  subne0d  8339  subne0ad  8341  subneintrd  8374  subneintr2d  8376  qapne  9704  xrlttri3  9863  xaddass2  9936  seqf1oglem1  10590  sqne0  10676  fihashneq0  10865  hashnncl  10866  cjne0  11052  absne0d  11331  sqrt2irraplemnn  12317  4sqlem11  12539  ringinvnz1ne0  13545  metn0  14546  lgsabs1  15155  neap0mkv  15559