Theorem eqnetri 3021

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 3015	. 2 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)
4	1, 3	mpbir 234	1 ⊢ 𝐴 ≠ 𝐶

Syntax hints:   = wceq 1538   ≠ wne 2951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2750  df-ne 2952

This theorem is referenced by:  eqnetrri  3022  notzfaus  5230  notzfausOLD  5231  2on0  8123  1n0  8129  noinfep  9156  card1  9430  fin23lem31  9803  s1nz  14008  bpoly4  15461  tan0  15552  resslem  16615  basendxnplusgndx  16666  plusgndxnmulrndx  16675  basendxnmulrndx  16676  slotsbhcdif  16751  symgvalstruct  18592  rmodislmod  19770  cnfldfun  20178  xrsnsgrp  20202  matvsca  21116  ustuqtop1  22942  iaa  25020  tan4thpi  25206  ang180lem2  25495  mcubic  25532  quart1lem  25540  ex-lcm  28342  9p10ne21  28354  resvlem  31056  esumnul  31535  ballotth  32023  quad3  33144  nogt01o  33464  bj-1upln0  34726  bj-2upln0  34740  bj-2upln1upl  34741  nn0rppwr  39830  sn-0ne2  39886  flt0  39966  flt4lem5e  39985  mncn0  40456  aaitgo  40479  mnringnmulrd  41295  stirlinglem11  43092  sec0  45677  2p2ne5  45717