Theorem eqnetri 3015

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

Syntax hints:   = wceq 1539   ≠ wne 2944

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-ne 2945

This theorem is referenced by:  eqnetrri  3016  notzfaus  5286  2on0  8322  1n0  8327  snnen2o  9035  noinfep  9427  card1  9735  fin23lem31  10108  s1nz  14321  bpoly4  15778  tan0  15869  resslemOLD  16961  basendxnplusgndxOLD  17002  basendxnmulrndx  17014  basendxnmulrndxOLD  17015  plusgndxnmulrndx  17016  slotsbhcdif  17134  slotsbhcdifOLD  17135  symgvalstructOLD  19014  rmodislmodOLD  20201  cnfldfunALTOLD  20620  xrsnsgrp  20643  matvscaOLD  21574  ustuqtop1  23402  iaa  25494  tan4thpi  25680  ang180lem2  25969  mcubic  26006  quart1lem  26014  slotsinbpsd  26811  slotslnbpsd  26812  ex-lcm  28831  9p10ne21  28843  resvlemOLD  31540  esumnul  32025  ballotth  32513  quad3  33637  nogt01o  33908  bj-1upln0  35208  bj-2upln0  35222  bj-2upln1upl  35223  nn0rppwr  40340  sn-0ne2  40396  flt0  40481  flt4lem5e  40500  mncn0  40971  aaitgo  40994  mnringnmulrdOLD  41835  stirlinglem11  43632  sec0  46473  2p2ne5  46513