Theorem eqnetri 3057

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

Syntax hints:   = wceq 1538   ≠ wne 2987

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-ne 2988

This theorem is referenced by:  eqnetrri  3058  notzfaus  5227  notzfausOLD  5228  2on0  8096  1n0  8102  noinfep  9107  card1  9381  fin23lem31  9754  s1nz  13952  bpoly4  15405  tan0  15496  resslem  16549  basendxnplusgndx  16600  plusgndxnmulrndx  16609  basendxnmulrndx  16610  slotsbhcdif  16685  symgvalstruct  18517  rmodislmod  19695  cnfldfun  20103  xrsnsgrp  20127  matvsca  21021  ustuqtop1  22847  iaa  24921  tan4thpi  25107  ang180lem2  25396  mcubic  25433  quart1lem  25441  ex-lcm  28243  9p10ne21  28255  resvlem  30955  esumnul  31417  ballotth  31905  quad3  33026  bj-1upln0  34445  bj-2upln0  34459  bj-2upln1upl  34460  nn0rppwr  39490  sn-0ne2  39544  mncn0  40083  aaitgo  40106  mnringnmulrd  40922  stirlinglem11  42726  sec0  45286  2p2ne5  45326