Theorem eqnetri 2995

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

Syntax hints:   = wceq 1540   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  eqnetrri  2996  notzfaus  5305  2on0  8409  1n0  8413  snnen2o  9144  noinfep  9575  card1  9883  fin23lem31  10256  s1nz  14532  bpoly4  15984  tan0  16078  nn0rppwr  16490  basendxnmulrndx  17218  plusgndxnmulrndx  17219  slotsbhcdif  17337  xrsnsgrp  21332  pzriprnglem4  21409  ustuqtop1  24145  iaa  26249  tan4thpi  26439  tan4thpiOLD  26440  ang180lem2  26736  mcubic  26773  quart1lem  26781  nogt01o  27624  slotsinbpsd  28404  slotslnbpsd  28405  ex-lcm  30420  9p10ne21  30432  cos9thpiminplylem5  33755  esumnul  34017  ballotth  34508  quad3  35645  bj-1upln0  36985  bj-2upln0  36999  bj-2upln1upl  37000  tan3rdpi  42328  sn-0ne2  42382  flt0  42613  flt4lem5e  42632  mncn0  43115  aaitgo  43138  stirlinglem11  46069  cjnpoly  46877  pgnbgreunbgrlem4  48107  sec0  49749  2p2ne5  49787