Theorem neeq1i 1595

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

Syntax hints:   <-> wb 146   = wceq 958   =/= wne 1588

This theorem is referenced by:  rabn0 2296  notzfaus 2746  exss 2775  1ne0 4148  map0 4350  kmlem3 4777  zorn2lem6 4803  uzwo3lem1 6218  crrecz 6742  climsup 7155  bcth 8029  nmcopexlem4 9949  nmcfnexlem4 9978  fgsb 10555

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1472  df-ne 1590

Copyright terms: Public domain