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 1540   ≠ wne 2932

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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  eqnetrri  3003  notzfaus  5333  2on0  8496  1n0  8500  snnen2o  9245  noinfep  9674  card1  9982  fin23lem31  10357  s1nz  14625  bpoly4  16075  tan0  16169  nn0rppwr  16580  basendxnmulrndx  17310  plusgndxnmulrndx  17311  slotsbhcdif  17429  xrsnsgrp  21370  pzriprnglem4  21445  ustuqtop1  24180  iaa  26285  tan4thpi  26475  tan4thpiOLD  26476  ang180lem2  26772  mcubic  26809  quart1lem  26817  nogt01o  27660  slotsinbpsd  28420  slotslnbpsd  28421  ex-lcm  30439  9p10ne21  30451  cos9thpiminplylem5  33820  esumnul  34079  ballotth  34570  quad3  35692  bj-1upln0  37027  bj-2upln0  37041  bj-2upln1upl  37042  tan3rdpi  42399  sn-0ne2  42449  flt0  42660  flt4lem5e  42679  mncn0  43163  aaitgo  43186  stirlinglem11  46113  sec0  49624  2p2ne5  49662