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 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

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

This theorem is used by:  eqnetrri  3026  notsep  5325  2on0  8498  1n0  8502  1n0OLD  8503  snnen2o  9243  noinfep  9668  card1  10056  fin23lem31  10428  s1nz  14761  bpoly4  16234  tan0  16328  nn0rppwr  16744  basendxnmulrndx  17476  plusgndxnmulrndx  17477  slotsbhcdif  17595  xrsnsgrp  21723  pzriprnglem4  21799  ustuqtop1  24569  iaa  26660  iaaOLD  26661  tan4thpi  26852  ang180lem2  27147  mcubic  27184  quart1lem  27192  flt0  27978  nogt01o  28062  slotsinbpsd  28912  slotslnbpsd  28913  ex-lcm  31068  9p10ne21  31080  cos9thpiminplylem5  34468  esumnul  34730  ballotth  35220  quad3  36525  bj-1upln0  38018  bj-2upln0  38032  bj-2upln1upl  38033  tan3rdpi  43512  sn-0ne2  43566  mncn0  44250  aaitgo  44273  stirlinglem11  47202  cjnpoly  48047  pgnbgreunbgrlem4  49325  fuconuniqlem  50889  sec0  51036  2p2ne5  51119