Theorem eqnetri 3008

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

Syntax hints:   = wceq 1536   ≠ wne 2937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ne 2938

This theorem is referenced by:  eqnetrri  3009  notzfaus  5368  2on0  8520  1n0  8524  snnen2o  9270  noinfep  9697  card1  10005  fin23lem31  10380  s1nz  14641  bpoly4  16091  tan0  16183  nn0rppwr  16594  resslemOLD  17287  basendxnplusgndxOLD  17328  basendxnmulrndx  17340  basendxnmulrndxOLD  17341  plusgndxnmulrndx  17342  slotsbhcdif  17460  slotsbhcdifOLD  17461  symgvalstructOLD  19429  rmodislmodOLD  20945  cnfldfunALTOLDOLD  21410  xrsnsgrp  21437  pzriprnglem4  21512  matvscaOLD  22437  ustuqtop1  24265  iaa  26381  tan4thpi  26570  tan4thpiOLD  26571  ang180lem2  26867  mcubic  26904  quart1lem  26912  nogt01o  27755  slotsinbpsd  28463  slotslnbpsd  28464  ex-lcm  30486  9p10ne21  30498  resvlemOLD  33337  esumnul  34028  ballotth  34518  quad3  35654  bj-1upln0  36991  bj-2upln0  37005  bj-2upln1upl  37006  tan3rdpi  42364  sn-0ne2  42412  flt0  42623  flt4lem5e  42642  mncn0  43127  aaitgo  43150  mnringnmulrdOLD  44205  stirlinglem11  46039  sec0  48990  2p2ne5  49028