Theorem eqnetri 2753

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

Syntax hints:   = wceq 1395   =/= wne 2652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-cleq 2449  df-ne 2654

This theorem is referenced by:  eqnetrri  2754  notzfaus  4631  2on0  7157  1n0  7163  noinfep  8093  card1  8366  fin23lem31  8740  tan0  13898  resslem  14704  slotsbhcdif  14837  xrsnsgrp  18581  matbas  19042  matplusg  19043  matvsca  19045  ustuqtop1  20870  iaa  22847  tan4thpi  23033  ang180lem2  23268  mcubic  23304  quart1lem  23312  resvlem  27982  esumnul  28222  ballotth  28673  quad3  29221  bpoly4  30026  mncn0  31292  aaitgo  31315  stirlinglem11  32069  uhgrepe  32640  plusgndxnmulrndx  32903  basendxnmulrndx  32904  sec0  33298  2p2ne5  33357  bj-1upln0  34710  bj-2upln0  34724  bj-2upln1upl  34725