Theorem eqnetri 3012

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

Syntax hints:   = wceq 1542   ≠ wne 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2942

This theorem is referenced by:  eqnetrri  3013  notzfaus  5362  2on0  8482  1n0  8488  snnen2o  9237  noinfep  9655  card1  9963  fin23lem31  10338  s1nz  14557  bpoly4  16003  tan0  16094  resslemOLD  17187  basendxnplusgndxOLD  17228  basendxnmulrndx  17240  basendxnmulrndxOLD  17241  plusgndxnmulrndx  17242  slotsbhcdif  17360  slotsbhcdifOLD  17361  symgvalstructOLD  19265  rmodislmodOLD  20541  cnfldfunALTOLD  20958  xrsnsgrp  20981  matvscaOLD  21918  ustuqtop1  23746  iaa  25838  tan4thpi  26024  ang180lem2  26315  mcubic  26352  quart1lem  26360  nogt01o  27199  slotsinbpsd  27723  slotslnbpsd  27724  ex-lcm  29742  9p10ne21  29754  resvlemOLD  32477  esumnul  33077  ballotth  33567  quad3  34686  bj-1upln0  35938  bj-2upln0  35952  bj-2upln1upl  35953  nn0rppwr  41272  sn-0ne2  41327  flt0  41427  flt4lem5e  41446  mncn0  41929  aaitgo  41952  mnringnmulrdOLD  43017  stirlinglem11  44848  pzriprnglem4  46856  sec0  47853  2p2ne5  47893