Theorem neeqtrri 3012

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

Syntax hints:   = wceq 1537   ≠ wne 2938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ne 2939

This theorem is referenced by:  nlim1  8526  nlim2  8527  1one2o  8683  cflim2  10301  pnfnemnf  11314  resslemOLD  17288  basendxnplusgndxOLD  17329  basendxnmulrndx  17341  basendxnmulrndxOLD  17342  plusgndxnmulrndx  17343  slotsbhcdif  17461  slotsbhcdifOLD  17462  symgvalstructOLD  19430  rmodislmodOLD  20946  cnfldfunALTOLDOLD  21411  xrsnsgrp  21438  zlmlemOLD  21546  matvscaOLD  22438  tnglemOLD  24670  slotsinbpsd  28464  slotslnbpsd  28465  setsvtx  29067  resvlemOLD  33338  limsucncmpi  36428  sn-1ne2  42279  mnringbasedOLD  44208  mnringaddgdOLD  44214  mnringscadOLD  44219  mnringvscadOLD  44221