Theorem neeqtrri 3060

Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)

Hypotheses

Ref	Expression
neeqtrr.1	⊢ 𝐴 ≠ 𝐵
neeqtrr.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
neeqtrri	⊢ 𝐴 ≠ 𝐶

Proof of Theorem neeqtrri

Step	Hyp	Ref	Expression
1		neeqtrr.1	. 2 ⊢ 𝐴 ≠ 𝐵
2		neeqtrr.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2807	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	neeqtri 3059	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:  1one2o  8252  cflim2  9674  pnfnemnf  10685  resslem  16549  basendxnplusgndx  16600  plusgndxnmulrndx  16609  basendxnmulrndx  16610  slotsbhcdif  16685  symgvalstruct  18517  rmodislmod  19695  cnfldfun  20103  xrsnsgrp  20127  zlmlem  20210  matvsca  21021  tnglem  23246  setsvtx  26828  resvlem  30955  limsucncmpi  33906  sn-1ne2  39466  mnringbased  40923  mnringaddgd  40928  mnringscad  40932  mnringvscad  40933