Theorem eqnetri 2763

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 2752	. 2 |- ( A =/= C <-> B =/= C )
4	1, 3	mpbir 209	1 |- A =/= C

Syntax hints:   = wceq 1379   =/= wne 2662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-cleq 2459  df-ne 2664

This theorem is referenced by:  eqnetrri  2764  notzfaus  4628  2on0  7151  1n0  7157  noinfep  8088  card1  8361  fin23lem31  8735  tan0  13764  resslem  14565  xrsnsgrp  18324  matbas  18784  matplusg  18785  matvsca  18787  ustuqtop1  20612  iaa  22588  tan4thpi  22773  ang180lem2  23008  mcubic  23044  quart1lem  23052  resvlem  27646  esumnul  27884  ballotth  28301  bpoly4  29748  mncn0  31017  aaitgo  31040  stirlinglem11  31707  uhgrepe  32168  plusgndxnmulrndx  32353  basendxnmulrndx  32354  sec0  32636  2p2ne5  32695  bj-1upln0  34049  bj-2upln0  34063  bj-2upln1upl  34064