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

Syntax hints:   = wceq 1539   ≠ wne 2938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722  df-ne 2939

This theorem is referenced by:  nlim1  8491  nlim2  8492  1one2o  8647  cflim2  10260  pnfnemnf  11273  resslemOLD  17191  basendxnplusgndxOLD  17232  basendxnmulrndx  17244  basendxnmulrndxOLD  17245  plusgndxnmulrndx  17246  slotsbhcdif  17364  slotsbhcdifOLD  17365  symgvalstructOLD  19306  rmodislmodOLD  20685  cnfldfunALTOLD  21158  xrsnsgrp  21181  zlmlemOLD  21286  matvscaOLD  22138  tnglemOLD  24370  slotsinbpsd  27959  slotslnbpsd  27960  setsvtx  28562  resvlemOLD  32716  limsucncmpi  35633  sn-1ne2  41481  mnringbasedOLD  43273  mnringaddgdOLD  43279  mnringscadOLD  43284  mnringvscadOLD  43286