Theorem eqnetri 3004

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

Syntax hints:   = wceq 1547   ≠ wne 2934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ne 2935

This theorem is referenced by:  eqnetrri  3005  notzfaus  5292  2on0  8409  1n0  8413  snnen2o  9145  noinfep  9572  card1  9883  fin23lem31  10256  s1nz  14561  bpoly4  16015  tan0  16109  nn0rppwr  16521  basendxnmulrndx  17250  plusgndxnmulrndx  17251  slotsbhcdif  17369  xrsnsgrp  21383  pzriprnglem4  21459  ustuqtop1  24224  iaa  26309  tan4thpi  26496  tan4thpiOLD  26497  ang180lem2  26792  mcubic  26829  quart1lem  26837  nogt01o  27678  slotsinbpsd  28527  slotslnbpsd  28528  ex-lcm  30546  9p10ne21  30558  cos9thpiminplylem5  33970  esumnul  34232  ballotth  34722  quad3  35898  bj-1upln0  37362  bj-2upln0  37376  bj-2upln1upl  37377  tan3rdpi  42829  sn-0ne2  42883  flt0  43087  flt4lem5e  43106  mncn0  43584  aaitgo  43607  stirlinglem11  46527  nthrucw  47331  cjnpoly  47352  pgnbgreunbgrlem4  48610  sec0  50250  2p2ne5  50288