Theorem eqnetri 3002

Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)

Hypotheses

Ref	Expression
eqnetr.1	⊢ 𝐴 = 𝐵
eqnetr.2	⊢ 𝐵 ≠ 𝐶

Assertion

Ref	Expression
eqnetri	⊢ 𝐴 ≠ 𝐶

Proof of Theorem eqnetri

Step	Hyp	Ref	Expression
1		eqnetr.2	. 2 ⊢ 𝐵 ≠ 𝐶
2		eqnetr.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	neeq1i 2996	. 2 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)
4	1, 3	mpbir 231	1 ⊢ 𝐴 ≠ 𝐶

Syntax hints:   = wceq 1542   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ne 2933

This theorem is referenced by:  eqnetrri  3003  notzfaus  5305  2on0  8419  1n0  8423  snnen2o  9155  noinfep  9581  card1  9892  fin23lem31  10265  s1nz  14570  bpoly4  16024  tan0  16118  nn0rppwr  16530  basendxnmulrndx  17259  plusgndxnmulrndx  17260  slotsbhcdif  17378  xrsnsgrp  21388  pzriprnglem4  21464  ustuqtop1  24206  iaa  26291  tan4thpi  26478  tan4thpiOLD  26479  ang180lem2  26774  mcubic  26811  quart1lem  26819  nogt01o  27660  slotsinbpsd  28509  slotslnbpsd  28510  ex-lcm  30528  9p10ne21  30540  cos9thpiminplylem5  33930  esumnul  34192  ballotth  34682  quad3  35852  bj-1upln0  37316  bj-2upln0  37330  bj-2upln1upl  37331  tan3rdpi  42784  sn-0ne2  42838  flt0  43070  flt4lem5e  43089  mncn0  43567  aaitgo  43590  stirlinglem11  46512  nthrucw  47316  cjnpoly  47337  pgnbgreunbgrlem4  48595  sec0  50235  2p2ne5  50273