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

Syntax hints:   = wceq 1542   ≠ wne 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

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

This theorem is referenced by:  nlim1  8489  nlim2  8490  1one2o  8645  cflim2  10258  pnfnemnf  11269  resslemOLD  17187  basendxnplusgndxOLD  17228  basendxnmulrndx  17240  basendxnmulrndxOLD  17241  plusgndxnmulrndx  17242  slotsbhcdif  17360  slotsbhcdifOLD  17361  symgvalstructOLD  19265  rmodislmodOLD  20541  cnfldfunALTOLD  20958  xrsnsgrp  20981  zlmlemOLD  21067  matvscaOLD  21918  tnglemOLD  24150  slotsinbpsd  27692  slotslnbpsd  27693  setsvtx  28295  resvlemOLD  32446  limsucncmpi  35330  sn-1ne2  41179  mnringbasedOLD  42971  mnringaddgdOLD  42977  mnringscadOLD  42982  mnringvscadOLD  42984