Theorem necon3bid 2461

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 2421	. 2 |- ( A =/= B <-> -. A = B )
2		necon3bid.1	. . 3 |- ( ph -> ( A = B <-> C = D ) )
3	2	necon3bbid 2460	. 2 |- ( ph -> ( -. A = B <-> C =/= D ) )
4	1, 3	bitrid 192	1 |- ( ph -> ( A =/= B <-> C =/= D ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   <-> wb 105   = wceq 1402   =/= wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624

This proof depends on definitions:  df-bi 117  df-ne 2421

This theorem is used by:  nebidc  2500  suppval1  6479  addneintrd  8515  addneintr2d  8516  negne0bd  8631  negned  8635  subne0d  8647  subne0ad  8649  subneintrd  8682  subneintr2d  8684  qapne  10048  xrlttri3  10209  xaddass2  10282  seqf1oglem1  10969  sqne0  11055  fihashneq0  11247  hashnncl  11248  ccat1st1st  11423  pfxn0  11474  cjne0  11688  absne0d  11968  sqrt2irraplemnn  12975  4sqlem11  13200  ballotfilemfrcn0  13322  ringinvnz1ne0  14403  rrgsupp  14623  metn0  15528  perfectlem2  16198  lgsabs1  16256  umgrclwwlkge2  16741  neap0mkv  17217