Theorem eqnetri 3030

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

This proof depends on syntax axioms:   = wceq 1570   ≠ wne 2960

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ne 2961

This theorem is used by:  eqnetrri  3031  notsep  5336  2on0  8470  1n0  8474  1n0OLD  8475  snnen2o  9208  noinfep  9632  card1  9966  fin23lem31  10338  s1nz  14660  bpoly4  16131  tan0  16225  nn0rppwr  16637  basendxnmulrndx  17367  plusgndxnmulrndx  17368  slotsbhcdif  17486  xrsnsgrp  21588  pzriprnglem4  21664  ustuqtop1  24429  iaa  26519  tan4thpi  26710  tan4thpiOLD  26711  ang180lem2  27006  mcubic  27043  quart1lem  27051  nogt01o  27891  slotsinbpsd  28741  slotslnbpsd  28742  ex-lcm  30856  9p10ne21  30868  cos9thpiminplylem5  34216  esumnul  34478  ballotth  34969  quad3  36175  bj-1upln0  37678  bj-2upln0  37692  bj-2upln1upl  37693  tan3rdpi  43146  sn-0ne2  43200  flt0  43402  flt4lem5e  43421  mncn0  43899  aaitgo  43922  stirlinglem11  46831  cjnpoly  47659  pgnbgreunbgrlem4  48917  sec0  50571  2p2ne5  50651