Theorem eqnetri 3029

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  eqnetrri  3030  notsep  5332  2on0  8529  1n0  8533  1n0OLD  8534  snnen2o  9274  noinfep  9698  card1  10086  fin23lem31  10460  s1nz  14795  bpoly4  16269  tan0  16363  nn0rppwr  16779  basendxnmulrndx  17513  plusgndxnmulrndx  17514  slotsbhcdif  17636  xrsnsgrp  21766  pzriprnglem4  21845  ustuqtop1  24615  iaa  26708  iaaOLD  26709  tan4thpi  26900  ang180lem2  27195  mcubic  27232  quart1lem  27240  flt0  28026  nogt01o  28110  slotsinbpsd  28960  slotslnbpsd  28961  ex-lcm  31116  9p10ne21  31128  cos9thpiminplylem5  34529  esumnul  34791  ballotth  35281  suceldifsn0  35832  jf1  36051  jf1o  36052  k39o  36058  jltalephlem  36066  quad3  36643  bj-1upln0  38137  bj-2upln0  38151  bj-2upln1upl  38152  tan3rdpi  43669  sn-0ne2  43723  mncn0  44406  aaitgo  44429  stirlinglem11  47367  cjnpoly  48212  pgnbgreunbgrlem4  49490  bru3val  49753  fuconuniqlem  51112  tanh0  51251  sec0  51281  2p2ne5  51364