Theorem eqnetri 2893

Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)

Hypotheses

Ref	Expression
eqnetr.1	⊢ 𝐴 = 𝐵
eqnetr.2	⊢ 𝐵 ≠ 𝐶

Assertion

Ref	Expression
eqnetri	⊢ 𝐴 ≠ 𝐶

Proof of Theorem eqnetri

Step	Hyp	Ref	Expression
1		eqnetr.2	. 2 ⊢ 𝐵 ≠ 𝐶
2		eqnetr.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	neeq1i 2887	. 2 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)
4	1, 3	mpbir 221	1 ⊢ 𝐴 ≠ 𝐶

Syntax hints:   = wceq 1523   ≠ wne 2823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-ne 2824

This theorem is referenced by:  eqnetrri  2894  notzfaus  4870  2on0  7614  1n0  7620  noinfep  8595  card1  8832  fin23lem31  9203  s1nz  13423  bpoly4  14834  tan0  14925  resslem  15980  basendxnplusgndx  16036  plusgndxnmulrndx  16045  basendxnmulrndx  16046  slotsbhcdif  16127  rmodislmod  18979  cnfldfun  19806  xrsnsgrp  19830  matbas  20267  matplusg  20268  matvsca  20270  ustuqtop1  22092  iaa  24125  tan4thpi  24311  ang180lem2  24585  mcubic  24619  quart1lem  24627  ex-lcm  27445  resvlem  29959  esumnul  30238  ballotth  30727  quad3  31690  bj-1upln0  33122  bj-2upln0  33136  bj-2upln1upl  33137  mncn0  38026  aaitgo  38049  stirlinglem11  40619  sec0  42829  2p2ne5  42872