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  10054  xrlttri3  10215  xaddass2  10288  seqf1oglem1  10976  sqne0  11062  fihashneq0  11254  hashnncl  11255  ccat1st1st  11430  pfxn0  11481  cjne0  11695  absne0d  11975  sqrt2irraplemnn  12983  4sqlem11  13208  ballotfilemfrcn0  13330  ringinvnz1ne0  14460  rrgsupp  14682  metn0  15621  perfectlem2  16317  lgsabs1  16380  umgrclwwlkge2  16865  neap0mkv  17343