Theorem neeq1i 1589

Description: Inference for inequality.

Hypothesis

Ref	Expression
neeq1i.1	|- A = B

Assertion

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

Proof of Theorem neeq1i

Step	Hyp	Ref	Expression
1		neeq1i.1	. 2 |- A = B
2		neeq1 1587	. 2 |- (A = B -> (A =/= C <-> B =/= C))
3	1, 2	ax-mp 7	1 |- (A =/= C <-> B =/= C)

Syntax hints:   <-> wb 146   = wceq 954   =/= wne 1582

This theorem is referenced by:  rabn0 2288  notzfaus 2736  exss 2764  1ne0 4132  map0 4334  kmlem3 4747  zorn2lem6 4773  uzwo3lem1 6172  crrecz 6680  climsup 7099  bcth 7982  nmcopexlem4 9892  nmcfnexlem4 9921  fgsb 10480

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1467  df-ne 1584

Copyright terms: Public domain