Theorem eqnetri 3013

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

Syntax hints:   = wceq 1539   ≠ wne 2942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-ne 2943

This theorem is referenced by:  eqnetrri  3014  notzfaus  5280  2on0  8276  1n0  8286  noinfep  9348  card1  9657  fin23lem31  10030  s1nz  14240  bpoly4  15697  tan0  15788  resslemOLD  16878  basendxnplusgndxOLD  16919  basendxnmulrndx  16931  basendxnmulrndxOLD  16932  plusgndxnmulrndx  16933  slotsbhcdif  17044  slotsbhcdifOLD  17045  symgvalstructOLD  18920  rmodislmodOLD  20107  cnfldfun  20522  xrsnsgrp  20546  matvsca  21473  ustuqtop1  23301  iaa  25390  tan4thpi  25576  ang180lem2  25865  mcubic  25902  quart1lem  25910  slotsinbpsd  26707  slotslnbpsd  26708  ex-lcm  28723  9p10ne21  28735  resvlemOLD  31433  esumnul  31916  ballotth  32404  quad3  33528  nogt01o  33826  bj-1upln0  35126  bj-2upln0  35140  bj-2upln1upl  35141  nn0rppwr  40254  sn-0ne2  40310  flt0  40390  flt4lem5e  40409  mncn0  40880  aaitgo  40903  mnringnmulrdOLD  41717  stirlinglem11  43515  sec0  46348  2p2ne5  46388