Theorem eqnetri 3086

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

Syntax hints:   = wceq 1533   ≠ wne 3016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-ne 3017

This theorem is referenced by:  eqnetrri  3087  notzfaus  5255  notzfausOLD  5256  2on0  8107  1n0  8113  noinfep  9117  card1  9391  fin23lem31  9759  s1nz  13955  bpoly4  15407  tan0  15498  resslem  16551  basendxnplusgndx  16602  plusgndxnmulrndx  16611  basendxnmulrndx  16612  slotsbhcdif  16687  symgvalstruct  18519  rmodislmod  19696  cnfldfun  20551  xrsnsgrp  20575  matvsca  21019  ustuqtop1  22844  iaa  24908  tan4thpi  25094  ang180lem2  25382  mcubic  25419  quart1lem  25427  ex-lcm  28231  9p10ne21  28243  resvlem  30899  esumnul  31302  ballotth  31790  quad3  32908  bj-1upln0  34316  bj-2upln0  34330  bj-2upln1upl  34331  nn0rppwr  39175  sn-0ne2  39229  mncn0  39732  aaitgo  39755  stirlinglem11  42362  sec0  44852  2p2ne5  44892