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

Syntax hints:   = wceq 1540   ≠ wne 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-cleq 2729  df-ne 2942

This theorem is referenced by:  nlim1  8365  nlim2  8366  1one2o  8522  cflim2  10089  pnfnemnf  11100  resslemOLD  17019  basendxnplusgndxOLD  17060  basendxnmulrndx  17072  basendxnmulrndxOLD  17073  plusgndxnmulrndx  17074  slotsbhcdif  17192  slotsbhcdifOLD  17193  symgvalstructOLD  19072  rmodislmodOLD  20263  cnfldfunALTOLD  20682  xrsnsgrp  20705  zlmlemOLD  20790  matvscaOLD  21636  tnglemOLD  23868  slotsinbpsd  26910  slotslnbpsd  26911  setsvtx  27513  resvlemOLD  31635  limsucncmpi  34695  sn-1ne2  40505  mnringbasedOLD  42058  mnringaddgdOLD  42064  mnringscadOLD  42069  mnringvscadOLD  42071