Theorem neeq1i 1584

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 1582	. 2 |- (A = B -> (A =/= C <-> B =/= C))
3	1, 2	ax-mp 7	1 |- (A =/= C <-> B =/= C)

Syntax hints:   <-> wb 146   = wceq 953   =/= wne 1577

This theorem is referenced by:  rabn0 2282  notzfaus 2731  exss 2759  1ne0 4126  map0 4328  kmlem3 4739  zorn2lem6 4765  uzwo3lem1 6164  crrecz 6672  climsup 7091  bcth 7966  nmcopexlem4 9869  nmcfnexlem4 9898  fgsb 10444

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1462  df-ne 1579

Copyright terms: Public domain