Theorem neeq2 2390

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 2215	. . 3 |- ( A = B -> ( C = A <-> C = B ) )
2	1	notbid 669	. 2 |- ( A = B -> ( -. C = A <-> -. C = B ) )
3		df-ne 2377	. 2 |- ( C =/= A <-> -. C = A )
4		df-ne 2377	. 2 |- ( C =/= B <-> -. C = B )
5	2, 3, 4	3bitr4g 223	1 |- ( A = B -> ( C =/= A <-> C =/= B ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 105   = wceq 1373   =/= wne 2376

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 615  ax-in2 616  ax-5 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-ne 2377

This theorem is referenced by:  neeq2i  2392  neeq2d  2395  disji2  4037  fodjuomnilemdc  7246  netap  7366  2oneel  7368  2omotaplemap  7369  2omotaplemst  7370  exmidapne  7372  xrlttri3  9919  hashdmprop2dom  10989  fun2dmnop0  10992  isnzr2  13946  neapmkv  16011  neap0mkv  16012  ltlenmkv  16013