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  8209  addneintr2d  8210  negne0bd  8325  negned  8329  subne0d  8341  subne0ad  8343  subneintrd  8376  subneintr2d  8378  qapne  9707  xrlttri3  9866  xaddass2  9939  seqf1oglem1  10593  sqne0  10679  fihashneq0  10868  hashnncl  10869  cjne0  11055  absne0d  11334  sqrt2irraplemnn  12320  4sqlem11  12542  ringinvnz1ne0  13548  metn0  14557  lgsabs1  15196  neap0mkv  15629