Theorem neeq1i 2630

Description: Inference for inequality. (Contributed by NM, 29-Apr-2005.)

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

Syntax hints:   <-> wb 184   = wceq 1369   =/= wne 2618

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2436  df-ne 2620

This theorem is referenced by:  neeq12i  2632  eqnetri  2637  syl5eqner  2645  rabn0  3669  exss  4567  suppvalbr  6706  brwitnlem  6959  en3lplem2  7833  hta  8116  kmlem3  8333  domtriomlem  8623  zorn2lem6  8682  konigthlem  8744  rpnnen1lem1  10991  rpnnen1lem2  10992  rpnnen1lem3  10993  rpnnen1lem5  10995  seqf1olem1  11857  iscyg2  16371  gsumval3lem2  16396  opprirred  16806  ptclsg  19200  iscusp2  19889  dchrptlem1  22615  dchrptlem2  22616  disjex  25946  disjexc  25947  eulerpartlems  26755  signsply0  26964  signstfveq0a  26989  fin2so  28428  inisegn0  29408  stoweidlem36  29843  aovnuoveq  30109  aovovn0oveq  30112  fsuppmapnn0fiubex  30812  bnj1177  32009  bnj1253  32020