Theorem eqnetri 3003

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

Syntax hints:   = wceq 1542   ≠ wne 2933

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 2709

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

This theorem is referenced by:  eqnetrri  3004  notzfaus  5300  2on0  8412  1n0  8416  snnen2o  9148  noinfep  9572  card1  9883  fin23lem31  10256  s1nz  14561  bpoly4  16015  tan0  16109  nn0rppwr  16521  basendxnmulrndx  17250  plusgndxnmulrndx  17251  slotsbhcdif  17369  xrsnsgrp  21397  pzriprnglem4  21474  ustuqtop1  24216  iaa  26302  tan4thpi  26491  tan4thpiOLD  26492  ang180lem2  26787  mcubic  26824  quart1lem  26832  nogt01o  27674  slotsinbpsd  28523  slotslnbpsd  28524  ex-lcm  30543  9p10ne21  30555  cos9thpiminplylem5  33946  esumnul  34208  ballotth  34698  quad3  35868  bj-1upln0  37332  bj-2upln0  37346  bj-2upln1upl  37347  tan3rdpi  42798  sn-0ne2  42852  flt0  43084  flt4lem5e  43103  mncn0  43585  aaitgo  43608  stirlinglem11  46530  nthrucw  47332  cjnpoly  47349  pgnbgreunbgrlem4  48607  sec0  50247  2p2ne5  50285