Theorem eqnetri 3010

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

Syntax hints:   = wceq 1540   ≠ wne 2939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723  df-ne 2940

This theorem is referenced by:  eqnetrri  3011  notzfaus  5361  2on0  8488  1n0  8494  snnen2o  9243  noinfep  9661  card1  9969  fin23lem31  10344  s1nz  14564  bpoly4  16010  tan0  16101  resslemOLD  17194  basendxnplusgndxOLD  17235  basendxnmulrndx  17247  basendxnmulrndxOLD  17248  plusgndxnmulrndx  17249  slotsbhcdif  17367  slotsbhcdifOLD  17368  symgvalstructOLD  19313  rmodislmodOLD  20773  cnfldfunALTOLD  21247  xrsnsgrp  21270  pzriprnglem4  21344  matvscaOLD  22238  ustuqtop1  24066  iaa  26177  tan4thpi  26364  ang180lem2  26656  mcubic  26693  quart1lem  26701  nogt01o  27543  slotsinbpsd  28126  slotslnbpsd  28127  ex-lcm  30145  9p10ne21  30157  resvlemOLD  32883  esumnul  33511  ballotth  34001  quad3  35120  bj-1upln0  36356  bj-2upln0  36370  bj-2upln1upl  36371  nn0rppwr  41689  sn-0ne2  41744  flt0  41844  flt4lem5e  41863  mncn0  42346  aaitgo  42369  mnringnmulrdOLD  43434  stirlinglem11  45261  sec0  47969  2p2ne5  48009