Theorem neeq2 2434

Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.)

Assertion

Ref	Expression
neeq2	|- ( A = B -> ( C =/= A <-> C =/= B ) )

Proof of Theorem neeq2

Step	Hyp	Ref	Expression
1		eqeq2 2248	. . 3 |- ( A = B -> ( C = A <-> C = B ) )
2	1	notbid 677	. 2 |- ( A = B -> ( -. C = A <-> -. C = B ) )
3		df-ne 2421	. 2 |- ( C =/= A <-> -. C = A )
4		df-ne 2421	. 2 |- ( C =/= B <-> -. C = B )
5	2, 3, 4	3bitr4g 223	1 |- ( A = B -> ( C =/= A <-> C =/= B ) )

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  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is used by:  neeq2i  2436  neeq2d  2439  disji2  4122  fodjuomnilemdc  7490  netap  7626  2oneel  7628  2omotaplemap  7629  2omotaplemst  7630  exmidapne  7632  xrlttri3  10215  hashdmprop2dom  11317  fun2dmnop0  11323  isnzr2  14599  umgrvad2edg  16674  eupth2lem3lem4fi  16936  3dom  17240  qdiff  17322  neapmkv  17342  neap0mkv  17343  ltlenmkv  17344