Theorem eqnetri 2852

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

Syntax hints:   = wceq 1475   ≠ wne 2780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782

This theorem is referenced by:  eqnetrri  2853  notzfaus  4766  2on0  7456  1n0  7462  noinfep  8440  card1  8677  fin23lem31  9048  s1nz  13239  bpoly4  14629  tan0  14720  resslem  15760  slotsbhcdif  15903  xrsnsgrp  19601  matbas  20038  matplusg  20039  matvsca  20041  ustuqtop1  21855  iaa  23884  tan4thpi  24070  ang180lem2  24340  mcubic  24374  quart1lem  24382  ex-lcm  26707  resvlem  29162  esumnul  29437  ballotth  29926  quad3  30818  bj-1upln0  32190  bj-2upln0  32204  bj-2upln1upl  32205  mncn0  36728  aaitgo  36751  stirlinglem11  38977  plusgndxnmulrndx  41743  basendxnmulrndx  41744  sec0  42300  2p2ne5  42353