Theorem eqnetri 3011

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 3005	. 2 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)
4	1, 3	mpbir 231	1 ⊢ 𝐴 ≠ 𝐶

Syntax hints:   = wceq 1540   ≠ wne 2940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ne 2941

This theorem is referenced by:  eqnetrri  3012  notzfaus  5363  2on0  8522  1n0  8526  snnen2o  9273  noinfep  9700  card1  10008  fin23lem31  10383  s1nz  14645  bpoly4  16095  tan0  16187  nn0rppwr  16598  resslemOLD  17288  basendxnmulrndx  17339  basendxnmulrndxOLD  17340  plusgndxnmulrndx  17341  slotsbhcdif  17459  slotsbhcdifOLD  17460  symgvalstructOLD  19415  cnfldfunALTOLDOLD  21393  xrsnsgrp  21420  pzriprnglem4  21495  matvscaOLD  22422  ustuqtop1  24250  iaa  26367  tan4thpi  26556  tan4thpiOLD  26557  ang180lem2  26853  mcubic  26890  quart1lem  26898  nogt01o  27741  slotsinbpsd  28449  slotslnbpsd  28450  ex-lcm  30477  9p10ne21  30489  resvlemOLD  33358  esumnul  34049  ballotth  34540  quad3  35675  bj-1upln0  37010  bj-2upln0  37024  bj-2upln1upl  37025  tan3rdpi  42386  sn-0ne2  42436  flt0  42647  flt4lem5e  42666  mncn0  43151  aaitgo  43174  mnringnmulrdOLD  44229  stirlinglem11  46099  sec0  49279  2p2ne5  49317