Theorem eqnetri 2694

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

Syntax hints:   = wceq 1448   =/= wne 2622

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

This theorem depends on definitions:  df-bi 190  df-cleq 2445  df-ne 2624

This theorem is referenced by:  eqnetrri  2695  notzfaus  4551  2on0  7178  1n0  7184  noinfep  8152  card1  8389  fin23lem31  8760  bpoly4  14123  tan0  14216  resslem  15193  slotsbhcdif  15329  xrsnsgrp  19015  matbas  19449  matplusg  19450  matvsca  19452  ustuqtop1  21267  iaa  23293  tan4thpi  23481  ang180lem2  23751  mcubic  23785  quart1lem  23793  resvlem  28601  esumnul  28876  ballotth  29376  ballotthOLD  29414  quad3  30308  bj-1upln0  31605  bj-2upln0  31619  bj-2upln1upl  31620  mncn0  36000  aaitgo  36030  stirlinglem11  38003  plusgndxnmulrndx  40278  basendxnmulrndx  40279  sec0  40805  2p2ne5  40862