Theorem neeqtrri 3018

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

Syntax hints:   = wceq 1541   ≠ wne 2944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-cleq 2731  df-ne 2945

This theorem is referenced by:  1one2o  8450  cflim2  10003  pnfnemnf  11014  resslemOLD  16933  basendxnplusgndxOLD  16974  basendxnmulrndx  16986  basendxnmulrndxOLD  16987  plusgndxnmulrndx  16988  slotsbhcdif  17106  slotsbhcdifOLD  17107  symgvalstructOLD  18986  rmodislmodOLD  20173  cnfldfunOLD  20591  xrsnsgrp  20615  zlmlemOLD  20700  matvscaOLD  21546  tnglemOLD  23778  slotsinbpsd  26783  slotslnbpsd  26784  setsvtx  27386  resvlemOLD  31510  limsucncmpi  34613  sn-1ne2  40275  mnringbasedOLD  41783  mnringaddgdOLD  41789  mnringscadOLD  41794  mnringvscadOLD  41796