Theorem eqnetri 2727

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

Syntax hints:   = wceq 1437   =/= wne 2625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-cleq 2421  df-ne 2627

This theorem is referenced by:  eqnetrri  2728  notzfaus  4600  2on0  7199  1n0  7205  noinfep  8164  card1  8401  fin23lem31  8771  bpoly4  14090  tan0  14183  resslem  15144  slotsbhcdif  15277  xrsnsgrp  18939  matbas  19369  matplusg  19370  matvsca  19372  ustuqtop1  21187  iaa  23146  tan4thpi  23334  ang180lem2  23604  mcubic  23638  quart1lem  23646  resvlem  28433  esumnul  28708  ballotth  29196  quad3  30090  bj-1upln0  31352  bj-2upln0  31366  bj-2upln1upl  31367  mncn0  35703  aaitgo  35726  stirlinglem11  37514  uhgrepe  38447  plusgndxnmulrndx  38710  basendxnmulrndx  38711  sec0  39240  2p2ne5  39297