Theorem neeqtrri 3015

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

Syntax hints:   = wceq 1539   ≠ wne 2941

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 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780  df-cleq 2728  df-ne 2942

This theorem is referenced by:  nlim1  8350  nlim2  8351  1one2o  8507  cflim2  10065  pnfnemnf  11076  resslemOLD  16997  basendxnplusgndxOLD  17038  basendxnmulrndx  17050  basendxnmulrndxOLD  17051  plusgndxnmulrndx  17052  slotsbhcdif  17170  slotsbhcdifOLD  17171  symgvalstructOLD  19050  rmodislmodOLD  20237  cnfldfunALTOLD  20656  xrsnsgrp  20679  zlmlemOLD  20764  matvscaOLD  21610  tnglemOLD  23842  slotsinbpsd  26847  slotslnbpsd  26848  setsvtx  27450  resvlemOLD  31576  limsucncmpi  34679  sn-1ne2  40332  mnringbasedOLD  41868  mnringaddgdOLD  41874  mnringscadOLD  41879  mnringvscadOLD  41881