Theorem eqnetri 3034

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

Syntax hints:   = wceq 1567   ≠ wne 2964

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ne 2965

This theorem is referenced by:  eqnetrri  3035  notzfaus  5332  2on0  8464  1n0  8468  1n0OLD  8469  snnen2o  9201  noinfep  9625  card1  9950  fin23lem31  10323  s1nz  14641  bpoly4  16109  tan0  16203  nn0rppwr  16615  basendxnmulrndx  17345  plusgndxnmulrndx  17346  slotsbhcdif  17464  xrsnsgrp  21523  pzriprnglem4  21599  ustuqtop1  24363  iaa  26451  tan4thpi  26641  tan4thpiOLD  26642  ang180lem2  26937  mcubic  26974  quart1lem  26982  nogt01o  27822  slotsinbpsd  28672  slotslnbpsd  28673  ex-lcm  30746  9p10ne21  30758  cos9thpiminplylem5  34117  esumnul  34379  ballotth  34869  quad3  36057  bj-1upln0  37529  bj-2upln0  37543  bj-2upln1upl  37544  tan3rdpi  42996  sn-0ne2  43050  flt0  43254  flt4lem5e  43273  mncn0  43751  aaitgo  43774  stirlinglem11  46683  nthrucw  47487  cjnpoly  47508  pgnbgreunbgrlem4  48766  sec0  50416  2p2ne5  50454