Theorem eqnetri 3026

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

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

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 2733

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

This theorem is used by:  eqnetrri  3027  notsep  5325  2on0  8484  1n0  8488  1n0OLD  8489  snnen2o  9229  noinfep  9654  card1  10042  fin23lem31  10414  s1nz  14747  bpoly4  16218  tan0  16312  nn0rppwr  16728  basendxnmulrndx  17460  plusgndxnmulrndx  17461  slotsbhcdif  17579  xrsnsgrp  21707  pzriprnglem4  21783  ustuqtop1  24553  iaa  26644  iaaOLD  26645  tan4thpi  26836  ang180lem2  27131  mcubic  27168  quart1lem  27176  flt0  27962  flt4lem5e  27979  nogt01o  28046  slotsinbpsd  28896  slotslnbpsd  28897  ex-lcm  31052  9p10ne21  31064  cos9thpiminplylem5  34411  esumnul  34673  ballotth  35163  quad3  36414  bj-1upln0  37902  bj-2upln0  37916  bj-2upln1upl  37917  tan3rdpi  43383  sn-0ne2  43437  mncn0  44125  aaitgo  44148  stirlinglem11  47063  cjnpoly  47908  pgnbgreunbgrlem4  49186  sec0  50822  2p2ne5  50905