Theorem necon3bid 2443

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 2403	. 2 |- ( A =/= B <-> -. A = B )
2		necon3bid.1	. . 3 |- ( ph -> ( A = B <-> C = D ) )
3	2	necon3bbid 2442	. 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 1397   =/= wne 2402

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 619  ax-in2 620

This theorem depends on definitions:  df-bi 117  df-ne 2403

This theorem is referenced by:  nebidc  2482  addneintrd  8367  addneintr2d  8368  negne0bd  8483  negned  8487  subne0d  8499  subne0ad  8501  subneintrd  8534  subneintr2d  8536  qapne  9873  xrlttri3  10032  xaddass2  10105  seqf1oglem1  10781  sqne0  10867  fihashneq0  11056  hashnncl  11057  ccat1st1st  11218  pfxn0  11269  cjne0  11469  absne0d  11748  sqrt2irraplemnn  12752  4sqlem11  12975  ringinvnz1ne0  14064  metn0  15104  perfectlem2  15726  lgsabs1  15770  umgrclwwlkge2  16255  neap0mkv  16676