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  4211  frecabcl  6487  fiintim  7030  eldju2ndl  7176  updjudhf  7183  netap  7368  2oneel  7370  2omotaplemap  7371  2omotaplemst  7372  exmidapne  7374  xnn0nemnf  9371  uzn0  9666  xrnemnf  9901  xrnepnf  9902  ngtmnft  9941  xsubge0  10005  xposdif  10006  xleaddadd  10011  fztpval  10207  hashdmprop2dom  10991  fun2dmnop0  10994  pcpre1  12648  pcqmul  12659  pcqcl  12662  xpsfrnel  13209  isnzr2  13979  fiinopn  14509  neapmkv  16044  neap0mkv  16045  ltlenmkv  16046