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  6483  addneintrd  8521  addneintr2d  8522  negne0bd  8637  negned  8641  subne0d  8653  subne0ad  8655  subneintrd  8688  subneintr2d  8690  qapne  10055  xrlttri3  10216  xaddass2  10289  seqf1oglem1  10977  sqne0  11063  fihashneq0  11255  hashnncl  11256  ccat1st1st  11431  pfxn0  11482  cjne0  11696  absne0d  11976  sqrt2irraplemnn  12984  4sqlem11  13209  ballotfilemfrcn0  13331  ringinvnz1ne0  14461  rrgsupp  14683  metn0  15604  perfectlem2  16300  lgsabs1  16363  umgrclwwlkge2  16848  neap0mkv  17326