Theorem eqnetri 3039

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

Syntax hints:   = wceq 1653   ≠ wne 2969

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-ext 2775

This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-cleq 2790  df-ne 2970

This theorem is referenced by:  eqnetrri  3040  notzfaus  5030  2on0  7807  1n0  7813  noinfep  8805  card1  9078  fin23lem31  9451  s1nz  13623  bpoly4  15123  tan0  15214  resslem  16255  basendxnplusgndx  16307  plusgndxnmulrndx  16316  basendxnmulrndx  16317  slotsbhcdif  16392  rmodislmod  19246  cnfldfun  20077  xrsnsgrp  20101  matbas  20541  matplusg  20542  matvsca  20544  ustuqtop1  22370  iaa  24418  tan4thpi  24605  ang180lem2  24889  mcubic  24923  quart1lem  24931  ex-lcm  27835  resvlem  30339  esumnul  30618  ballotth  31108  quad3  32071  bj-1upln0  33481  bj-2upln0  33495  bj-2upln1upl  33496  mncn0  38482  aaitgo  38505  stirlinglem11  41032  sec0  43291  2p2ne5  43334