Theorem eqnetri 2996

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

Syntax hints:   = wceq 1540   ≠ wne 2926

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 2702

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

This theorem is referenced by:  eqnetrri  2997  notzfaus  5321  2on0  8451  1n0  8455  snnen2o  9191  noinfep  9620  card1  9928  fin23lem31  10303  s1nz  14579  bpoly4  16032  tan0  16126  nn0rppwr  16538  basendxnmulrndx  17266  plusgndxnmulrndx  17267  slotsbhcdif  17385  xrsnsgrp  21326  pzriprnglem4  21401  ustuqtop1  24136  iaa  26240  tan4thpi  26430  tan4thpiOLD  26431  ang180lem2  26727  mcubic  26764  quart1lem  26772  nogt01o  27615  slotsinbpsd  28375  slotslnbpsd  28376  ex-lcm  30394  9p10ne21  30406  cos9thpiminplylem5  33783  esumnul  34045  ballotth  34536  quad3  35664  bj-1upln0  37004  bj-2upln0  37018  bj-2upln1upl  37019  tan3rdpi  42347  sn-0ne2  42401  flt0  42632  flt4lem5e  42651  mncn0  43135  aaitgo  43158  stirlinglem11  46089  pgnbgreunbgrlem4  48113  sec0  49753  2p2ne5  49791