Theorem eqnetri 3028

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

Syntax hints:   = wceq 1570   ≠ wne 2958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ne 2959

This theorem is referenced by:  eqnetrri  3029  notsep  5334  2on0  8464  1n0  8468  1n0OLD  8469  snnen2o  9201  noinfep  9625  card1  9950  fin23lem31  10322  s1nz  14641  bpoly4  16108  tan0  16202  nn0rppwr  16614  basendxnmulrndx  17344  plusgndxnmulrndx  17345  slotsbhcdif  17463  xrsnsgrp  21558  pzriprnglem4  21634  ustuqtop1  24398  iaa  26488  tan4thpi  26679  tan4thpiOLD  26680  ang180lem2  26975  mcubic  27012  quart1lem  27020  nogt01o  27860  slotsinbpsd  28710  slotslnbpsd  28711  ex-lcm  30809  9p10ne21  30821  cos9thpiminplylem5  34176  esumnul  34438  ballotth  34928  quad3  36162  bj-1upln0  37645  bj-2upln0  37659  bj-2upln1upl  37660  tan3rdpi  43113  sn-0ne2  43167  flt0  43369  flt4lem5e  43388  mncn0  43866  aaitgo  43889  stirlinglem11  46798  cjnpoly  47626  pgnbgreunbgrlem4  48884  sec0  50538  2p2ne5  50618