Theorem eqnetri 3026

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

Syntax hints:   = wceq 1559   ≠ wne 2956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ne 2957

This theorem is referenced by:  eqnetrri  3027  notzfaus  5317  2on0  8446  1n0  8450  1n0OLD  8451  snnen2o  9183  noinfep  9609  card1  9920  fin23lem31  10294  s1nz  14615  bpoly4  16080  tan0  16174  nn0rppwr  16586  basendxnmulrndx  17316  plusgndxnmulrndx  17317  slotsbhcdif  17435  xrsnsgrp  21448  pzriprnglem4  21524  ustuqtop1  24289  iaa  26377  tan4thpi  26567  tan4thpiOLD  26568  ang180lem2  26863  mcubic  26900  quart1lem  26908  nogt01o  27748  slotsinbpsd  28598  slotslnbpsd  28599  ex-lcm  30617  9p10ne21  30629  cos9thpiminplylem5  34044  esumnul  34306  ballotth  34796  quad3  35981  bj-1upln0  37455  bj-2upln0  37469  bj-2upln1upl  37470  tan3rdpi  42922  sn-0ne2  42976  flt0  43180  flt4lem5e  43199  mncn0  43677  aaitgo  43700  stirlinglem11  46619  nthrucw  47423  cjnpoly  47444  pgnbgreunbgrlem4  48702  sec0  50342  2p2ne5  50380