Theorem neeq1 2389

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

Assertion

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

Proof of Theorem neeq1

Step	Hyp	Ref	Expression
1		eqeq1 2212	. . 3 |- ( A = B -> ( A = C <-> B = C ) )
2	1	notbid 669	. 2 |- ( A = B -> ( -. A = C <-> -. B = C ) )
3		df-ne 2377	. 2 |- ( A =/= C <-> -. A = C )
4		df-ne 2377	. 2 |- ( B =/= C <-> -. B = C )
5	2, 3, 4	3bitr4g 223	1 |- ( A = B -> ( A =/= C <-> B =/= C ) )

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:  neeq1i  2391  neeq1d  2394  nelrdva  2980  disji2  4037  0inp0  4210  frecabcl  6485  fiintim  7028  eldju2ndl  7174  updjudhf  7181  netap  7366  2oneel  7368  2omotaplemap  7369  2omotaplemst  7370  exmidapne  7372  xnn0nemnf  9369  uzn0  9664  xrnemnf  9899  xrnepnf  9900  ngtmnft  9939  xsubge0  10003  xposdif  10004  xleaddadd  10009  fztpval  10205  hashdmprop2dom  10989  fun2dmnop0  10992  pcpre1  12615  pcqmul  12626  pcqcl  12629  xpsfrnel  13176  isnzr2  13946  fiinopn  14476  neapmkv  16007  neap0mkv  16008  ltlenmkv  16009