Theorem neeq2i 2700

Description: Inference for inequality. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)

Hypothesis

Ref	Expression
neeq1i.1	|- A = B

Assertion

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

Proof of Theorem neeq2i

Step	Hyp	Ref	Expression
1		neeq1i.1	. . 3 |- A = B
2	1	eqeq2i 2473	. 2 |- ( C = A <-> C = B )
3	2	necon3bii 2687	1 |- ( C =/= A <-> C =/= B )

Syntax hints:   <-> wb 189   = wceq 1454   =/= wne 2632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-cleq 2454  df-ne 2634

This theorem is referenced by:  neeqtri  2707  suppvalbr  6944  disjdsct  28331  divnumden2  28429  nosgnn0  30593  upgr3v3e3cycl  39920  upgr4cycl4dv4e  39925