Theorem neeq1 2391

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 2214	. . 3 |- ( A = B -> ( A = C <-> B = C ) )
2	1	notbid 669	. 2 |- ( A = B -> ( -. A = C <-> -. B = C ) )
3		df-ne 2379	. 2 |- ( A =/= C <-> -. A = C )
4		df-ne 2379	. 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 2378

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-ne 2379

This theorem is referenced by:  neeq1i  2393  neeq1d  2396  nelrdva  2987  disji2  4051  0inp0  4226  frecabcl  6508  fiintim  7054  eldju2ndl  7200  updjudhf  7207  netap  7401  2oneel  7403  2omotaplemap  7404  2omotaplemst  7405  exmidapne  7407  xnn0nemnf  9404  uzn0  9699  xrnemnf  9934  xrnepnf  9935  ngtmnft  9974  xsubge0  10038  xposdif  10039  xleaddadd  10044  fztpval  10240  hashdmprop2dom  11026  fun2dmnop0  11029  pcpre1  12730  pcqmul  12741  pcqcl  12744  xpsfrnel  13291  isnzr2  14061  fiinopn  14591  neapmkv  16209  neap0mkv  16210  ltlenmkv  16211