Theorem neeqtrri 3020

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

Syntax hints:   = wceq 1537   ≠ wne 2946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ne 2947

This theorem is referenced by:  nlim1  8545  nlim2  8546  1one2o  8702  cflim2  10332  pnfnemnf  11345  resslemOLD  17301  basendxnplusgndxOLD  17342  basendxnmulrndx  17354  basendxnmulrndxOLD  17355  plusgndxnmulrndx  17356  slotsbhcdif  17474  slotsbhcdifOLD  17475  symgvalstructOLD  19439  rmodislmodOLD  20951  cnfldfunALTOLDOLD  21416  xrsnsgrp  21443  zlmlemOLD  21551  matvscaOLD  22443  tnglemOLD  24675  slotsinbpsd  28467  slotslnbpsd  28468  setsvtx  29070  resvlemOLD  33323  limsucncmpi  36411  sn-1ne2  42254  mnringbasedOLD  44181  mnringaddgdOLD  44187  mnringscadOLD  44192  mnringvscadOLD  44194