Theorem eqnetri 3003

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

Syntax hints:   = wceq 1542   ≠ wne 2933

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934

This theorem is referenced by:  eqnetrri  3004  notzfaus  5310  2on0  8421  1n0  8425  snnen2o  9157  noinfep  9581  card1  9892  fin23lem31  10265  s1nz  14543  bpoly4  15994  tan0  16088  nn0rppwr  16500  basendxnmulrndx  17228  plusgndxnmulrndx  17229  slotsbhcdif  17347  xrsnsgrp  21374  pzriprnglem4  21451  ustuqtop1  24197  iaa  26301  tan4thpi  26491  tan4thpiOLD  26492  ang180lem2  26788  mcubic  26825  quart1lem  26833  nogt01o  27676  slotsinbpsd  28525  slotslnbpsd  28526  ex-lcm  30545  9p10ne21  30557  cos9thpiminplylem5  33963  esumnul  34225  ballotth  34715  quad3  35883  bj-1upln0  37254  bj-2upln0  37268  bj-2upln1upl  37269  tan3rdpi  42719  sn-0ne2  42773  flt0  42992  flt4lem5e  43011  mncn0  43493  aaitgo  43516  stirlinglem11  46439  nthrucw  47241  cjnpoly  47246  pgnbgreunbgrlem4  48476  sec0  50116  2p2ne5  50154