Theorem eqnetri 3025

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

This proof depends on syntax axioms:   = wceq 1570   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ne 2956

This theorem is used by:  eqnetrri  3026  notsep  5328  2on0  8470  1n0  8474  1n0OLD  8475  snnen2o  9215  noinfep  9639  card1  9973  fin23lem31  10345  s1nz  14674  bpoly4  16145  tan0  16239  nn0rppwr  16651  basendxnmulrndx  17381  plusgndxnmulrndx  17382  slotsbhcdif  17500  xrsnsgrp  21621  pzriprnglem4  21697  ustuqtop1  24467  iaa  26560  iaaOLD  26561  tan4thpi  26752  ang180lem2  27047  mcubic  27084  quart1lem  27092  nogt01o  27932  slotsinbpsd  28782  slotslnbpsd  28783  ex-lcm  30938  9p10ne21  30950  cos9thpiminplylem5  34296  esumnul  34558  ballotth  35049  quad3  36249  bj-1upln0  37753  bj-2upln0  37767  bj-2upln1upl  37768  tan3rdpi  43227  sn-0ne2  43281  flt0  43483  flt4lem5e  43502  mncn0  43980  aaitgo  44003  stirlinglem11  46912  cjnpoly  47757  pgnbgreunbgrlem4  49035  sec0  50686  2p2ne5  50769