Theorem eqnetri 2864

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

Syntax hints:   = wceq 1483   =/= wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-ne 2795

This theorem is referenced by:  eqnetrri  2865  notzfaus  4840  2on0  7569  1n0  7575  noinfep  8557  card1  8794  fin23lem31  9165  s1nz  13386  bpoly4  14790  tan0  14881  resslem  15933  basendxnplusgndx  15989  plusgndxnmulrndx  15998  basendxnmulrndx  15999  slotsbhcdif  16080  rmodislmod  18931  cnfldfun  19758  xrsnsgrp  19782  matbas  20219  matplusg  20220  matvsca  20222  ustuqtop1  22045  iaa  24080  tan4thpi  24266  ang180lem2  24540  mcubic  24574  quart1lem  24582  ex-lcm  27315  resvlem  29831  esumnul  30110  ballotth  30599  quad3  31564  bj-1upln0  32997  bj-2upln0  33011  bj-2upln1upl  33012  mncn0  37709  aaitgo  37732  stirlinglem11  40301  sec0  42501  2p2ne5  42544