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  7248  netap  7368  2oneel  7370  2omotaplemap  7371  2omotaplemst  7372  exmidapne  7374  xrlttri3  9921  hashdmprop2dom  10991  fun2dmnop0  10994  isnzr2  13979  neapmkv  16044  neap0mkv  16045  ltlenmkv  16046