Theorem neeq1 2360

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 2184	. . 3 |- ( A = B -> ( A = C <-> B = C ) )
2	1	notbid 667	. 2 |- ( A = B -> ( -. A = C <-> -. B = C ) )
3		df-ne 2348	. 2 |- ( A =/= C <-> -. A = C )
4		df-ne 2348	. 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 1353   =/= wne 2347

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 614  ax-in2 615  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-ne 2348

This theorem is referenced by:  neeq1i  2362  neeq1d  2365  nelrdva  2946  disji2  3998  0inp0  4168  frecabcl  6402  fiintim  6930  eldju2ndl  7073  updjudhf  7080  netap  7255  2oneel  7257  2omotaplemap  7258  2omotaplemst  7259  exmidapne  7261  xnn0nemnf  9252  uzn0  9545  xrnemnf  9779  xrnepnf  9780  ngtmnft  9819  xsubge0  9883  xposdif  9884  xleaddadd  9889  fztpval  10085  pcpre1  12294  pcqmul  12305  pcqcl  12308  xpsfrnel  12768  fiinopn  13589  neapmkv  14901  neap0mkv  14902  ltlenmkv  14903