Theorem neeqtrri 3014

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

Syntax hints:   = wceq 1540   ≠ wne 2940

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 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ne 2941

This theorem is referenced by:  nlim1  8527  nlim2  8528  1one2o  8684  cflim2  10303  pnfnemnf  11316  resslemOLD  17288  basendxnmulrndx  17339  basendxnmulrndxOLD  17340  plusgndxnmulrndx  17341  slotsbhcdif  17459  slotsbhcdifOLD  17460  symgvalstructOLD  19415  cnfldfunALTOLDOLD  21393  xrsnsgrp  21420  zlmlemOLD  21528  matvscaOLD  22422  tnglemOLD  24654  slotsinbpsd  28449  slotslnbpsd  28450  setsvtx  29052  resvlemOLD  33358  limsucncmpi  36446  sn-1ne2  42300  mnringbasedOLD  44231  mnringaddgdOLD  44237  mnringscadOLD  44242  mnringvscadOLD  44244