Theorem eqnetri 2851

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

Syntax hints:   = wceq 1474   ≠ wne 2779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-cleq 2602  df-ne 2781

This theorem is referenced by:  eqnetrri  2852  notzfaus  4761  2on0  7433  1n0  7439  noinfep  8417  card1  8654  fin23lem31  9025  s1nz  13185  bpoly4  14575  tan0  14666  resslem  15706  slotsbhcdif  15849  xrsnsgrp  19547  matbas  19980  matplusg  19981  matvsca  19983  ustuqtop1  21797  iaa  23801  tan4thpi  23987  ang180lem2  24257  mcubic  24291  quart1lem  24299  ex-lcm  26473  resvlem  28968  esumnul  29243  ballotth  29732  quad3  30624  bj-1upln0  31986  bj-2upln0  32000  bj-2upln1upl  32001  mncn0  36524  aaitgo  36547  stirlinglem11  38774  plusgndxnmulrndx  41738  basendxnmulrndx  41739  sec0  42256  2p2ne5  42309