Theorem eqnetri 2995

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

Syntax hints:   = wceq 1540   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  eqnetrri  2996  notzfaus  5318  2on0  8448  1n0  8452  snnen2o  9184  noinfep  9613  card1  9921  fin23lem31  10296  s1nz  14572  bpoly4  16025  tan0  16119  nn0rppwr  16531  basendxnmulrndx  17259  plusgndxnmulrndx  17260  slotsbhcdif  17378  xrsnsgrp  21319  pzriprnglem4  21394  ustuqtop1  24129  iaa  26233  tan4thpi  26423  tan4thpiOLD  26424  ang180lem2  26720  mcubic  26757  quart1lem  26765  nogt01o  27608  slotsinbpsd  28368  slotslnbpsd  28369  ex-lcm  30387  9p10ne21  30399  cos9thpiminplylem5  33776  esumnul  34038  ballotth  34529  quad3  35657  bj-1upln0  36997  bj-2upln0  37011  bj-2upln1upl  37012  tan3rdpi  42340  sn-0ne2  42394  flt0  42625  flt4lem5e  42644  mncn0  43128  aaitgo  43151  stirlinglem11  46082  cjnpoly  46890  pgnbgreunbgrlem4  48109  sec0  49749  2p2ne5  49787