Theorem eqnetri 3017

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

Syntax hints:   = wceq 1537   ≠ wne 2946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ne 2947

This theorem is referenced by:  eqnetrri  3018  notzfaus  5381  2on0  8538  1n0  8544  snnen2o  9300  noinfep  9729  card1  10037  fin23lem31  10412  s1nz  14655  bpoly4  16107  tan0  16199  nn0rppwr  16608  resslemOLD  17301  basendxnplusgndxOLD  17342  basendxnmulrndx  17354  basendxnmulrndxOLD  17355  plusgndxnmulrndx  17356  slotsbhcdif  17474  slotsbhcdifOLD  17475  symgvalstructOLD  19439  rmodislmodOLD  20951  cnfldfunALTOLDOLD  21416  xrsnsgrp  21443  pzriprnglem4  21518  matvscaOLD  22443  ustuqtop1  24271  iaa  26385  tan4thpi  26574  tan4thpiOLD  26575  ang180lem2  26871  mcubic  26908  quart1lem  26916  nogt01o  27759  slotsinbpsd  28467  slotslnbpsd  28468  ex-lcm  30490  9p10ne21  30502  resvlemOLD  33323  esumnul  34012  ballotth  34502  quad3  35638  bj-1upln0  36975  bj-2upln0  36989  bj-2upln1upl  36990  tan3rdpi  42338  sn-0ne2  42382  flt0  42592  flt4lem5e  42611  mncn0  43096  aaitgo  43119  mnringnmulrdOLD  44179  stirlinglem11  46005  sec0  48852  2p2ne5  48892