Theorem neeqtrri 2867

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 2631	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	neeqtri 2866	1 ⊢ 𝐴 ≠ 𝐶

Syntax hints:   = wceq 1483   ≠ wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-ne 2795

This theorem is referenced by:  cflim2  9085  pnfnemnf  10094  resslem  15933  basendxnplusgndx  15989  plusgndxnmulrndx  15998  basendxnmulrndx  15999  slotsbhcdif  16080  rmodislmod  18931  cnfldfun  19758  xrsnsgrp  19782  zlmlem  19865  matbas  20219  matplusg  20220  matvsca  20222  tnglem  22444  setsvtx  25927  resvlem  29831  limsucncmpi  32444