Theorem neeq2 2414

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 2239	. . 3 |- ( A = B -> ( C = A <-> C = B ) )
2	1	notbid 671	. 2 |- ( A = B -> ( -. C = A <-> -. C = B ) )
3		df-ne 2401	. 2 |- ( C =/= A <-> -. C = A )
4		df-ne 2401	. 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 1395   =/= wne 2400

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 617  ax-in2 618  ax-5 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-ne 2401

This theorem is referenced by:  neeq2i  2416  neeq2d  2419  disji2  4075  fodjuomnilemdc  7311  netap  7440  2oneel  7442  2omotaplemap  7443  2omotaplemst  7444  exmidapne  7446  xrlttri3  9993  hashdmprop2dom  11066  fun2dmnop0  11069  isnzr2  14148  umgrvad2edg  16009  neapmkv  16436  neap0mkv  16437  ltlenmkv  16438