Theorem eqnetri 2748

Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)

Hypotheses

Ref	Expression
eqnetr.1	|- A = B
eqnetr.2	|- B =/= C

Assertion

Ref	Expression
eqnetri	|- A =/= C

Proof of Theorem eqnetri

Step	Hyp	Ref	Expression
1		eqnetr.2	. 2 |- B =/= C
2		eqnetr.1	. . 3 |- A = B
3	2	neeq1i 2737	. 2 |- ( A =/= C <-> B =/= C )
4	1, 3	mpbir 209	1 |- A =/= C

Syntax hints:   = wceq 1370   =/= wne 2648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-cleq 2446  df-ne 2650

This theorem is referenced by:  eqnetrri  2749  notzfaus  4578  2on0  7042  1n0  7048  noinfep  7980  card1  8253  fin23lem31  8627  tan0  13557  resslem  14354  matbas  18449  matplusg  18450  matvsca  18452  ustuqtop1  19958  iaa  21934  tan4thpi  22119  ang180lem2  22349  mcubic  22385  quart1lem  22393  resvlem  26467  esumnul  26670  ballotth  27087  bpoly4  28369  mncn0  29667  aaitgo  29690  stirlinglem11  30050  sec0  31446  2p2ne5  31505  bj-1upln0  32859  bj-2upln0  32873  bj-2upln1upl  32874