Theorem eqnetri 2998

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

Syntax hints:   = wceq 1541   ≠ wne 2928

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 2121  ax-ext 2703

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

This theorem is referenced by:  eqnetrri  2999  notzfaus  5301  2on0  8399  1n0  8403  snnen2o  9129  noinfep  9550  card1  9861  fin23lem31  10234  s1nz  14515  bpoly4  15966  tan0  16060  nn0rppwr  16472  basendxnmulrndx  17200  plusgndxnmulrndx  17201  slotsbhcdif  17319  xrsnsgrp  21345  pzriprnglem4  21422  ustuqtop1  24157  iaa  26261  tan4thpi  26451  tan4thpiOLD  26452  ang180lem2  26748  mcubic  26785  quart1lem  26793  nogt01o  27636  slotsinbpsd  28420  slotslnbpsd  28421  ex-lcm  30436  9p10ne21  30448  cos9thpiminplylem5  33797  esumnul  34059  ballotth  34549  quad3  35712  bj-1upln0  37049  bj-2upln0  37063  bj-2upln1upl  37064  tan3rdpi  42391  sn-0ne2  42445  flt0  42676  flt4lem5e  42695  mncn0  43178  aaitgo  43201  stirlinglem11  46128  cjnpoly  46926  pgnbgreunbgrlem4  48156  sec0  49798  2p2ne5  49836