Theorem neeqtrri 2896

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

Syntax hints:   = wceq 1523   ≠ wne 2823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-ne 2824

This theorem is referenced by:  cflim2  9123  pnfnemnf  10132  resslem  15980  basendxnplusgndx  16036  plusgndxnmulrndx  16045  basendxnmulrndx  16046  slotsbhcdif  16127  rmodislmod  18979  cnfldfun  19806  xrsnsgrp  19830  zlmlem  19913  matbas  20267  matplusg  20268  matvsca  20270  tnglem  22491  setsvtx  25972  resvlem  29959  limsucncmpi  32569