Theorem eqnetri 2999

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

Syntax hints:   = wceq 1541   ≠ wne 2929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ne 2930

This theorem is referenced by:  eqnetrri  3000  notzfaus  5305  2on0  8407  1n0  8411  snnen2o  9138  noinfep  9559  card1  9870  fin23lem31  10243  s1nz  14519  bpoly4  15970  tan0  16064  nn0rppwr  16476  basendxnmulrndx  17204  plusgndxnmulrndx  17205  slotsbhcdif  17323  xrsnsgrp  21348  pzriprnglem4  21425  ustuqtop1  24159  iaa  26263  tan4thpi  26453  tan4thpiOLD  26454  ang180lem2  26750  mcubic  26787  quart1lem  26795  nogt01o  27638  slotsinbpsd  28422  slotslnbpsd  28423  ex-lcm  30442  9p10ne21  30454  cos9thpiminplylem5  33822  esumnul  34084  ballotth  34574  quad3  35737  bj-1upln0  37076  bj-2upln0  37090  bj-2upln1upl  37091  tan3rdpi  42473  sn-0ne2  42527  flt0  42758  flt4lem5e  42777  mncn0  43259  aaitgo  43282  stirlinglem11  46209  nthrucw  47011  cjnpoly  47016  pgnbgreunbgrlem4  48246  sec0  49888  2p2ne5  49926