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  27692  slotslnbpsd  27693  ex-lcm  29711  9p10ne21  29723  resvlemOLD  32446  esumnul  33046  ballotth  33536  quad3  34655  bj-1upln0  35890  bj-2upln0  35904  bj-2upln1upl  35905  nn0rppwr  41224  sn-0ne2  41279  flt0  41379  flt4lem5e  41398  mncn0  41881  aaitgo  41904  mnringnmulrdOLD  42969  stirlinglem11  44800  pzriprnglem4  46808  sec0  47805  2p2ne5  47845