Theorem eqnetri 3002

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

Syntax hints:   = wceq 1541   ≠ wne 2932

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 2708

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

This theorem is referenced by:  eqnetrri  3003  notzfaus  5308  2on0  8411  1n0  8415  snnen2o  9145  noinfep  9569  card1  9880  fin23lem31  10253  s1nz  14531  bpoly4  15982  tan0  16076  nn0rppwr  16488  basendxnmulrndx  17216  plusgndxnmulrndx  17217  slotsbhcdif  17335  xrsnsgrp  21362  pzriprnglem4  21439  ustuqtop1  24185  iaa  26289  tan4thpi  26479  tan4thpiOLD  26480  ang180lem2  26776  mcubic  26813  quart1lem  26821  nogt01o  27664  slotsinbpsd  28513  slotslnbpsd  28514  ex-lcm  30533  9p10ne21  30545  cos9thpiminplylem5  33943  esumnul  34205  ballotth  34695  quad3  35864  bj-1upln0  37210  bj-2upln0  37224  bj-2upln1upl  37225  tan3rdpi  42607  sn-0ne2  42661  flt0  42880  flt4lem5e  42899  mncn0  43381  aaitgo  43404  stirlinglem11  46328  nthrucw  47130  cjnpoly  47135  pgnbgreunbgrlem4  48365  sec0  50005  2p2ne5  50043