Theorem eqnetrrd 2993

Description: Substitution of equal classes into an inequality. (Contributed by NM, 4-Jul-2012.)

Hypotheses

Ref	Expression
eqnetrrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqnetrrd.2	⊢ (𝜑 → 𝐴 ≠ 𝐶)

Assertion

Ref	Expression
eqnetrrd	⊢ (𝜑 → 𝐵 ≠ 𝐶)

Proof of Theorem eqnetrrd

Step	Hyp	Ref	Expression
1		eqnetrrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	eqcomd 2735	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqnetrrd.2	. 2 ⊢ (𝜑 → 𝐴 ≠ 𝐶)
4	2, 3	eqnetrd 2992	1 ⊢ (𝜑 → 𝐵 ≠ 𝐶)

Syntax hints:   → wi 4   = 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:  eqnetrrid  3000  3netr3d  3001  cantnflem1c  9616  eqsqrt2d  15311  tanval2  16077  tanval3  16078  tanhlt1  16104  pcadd  16836  efgsres  19652  gsumval3  19821  ablfac  20004  ablsimpgfind  20026  isdrngrd  20686  isdrngrdOLD  20688  lspsneq  21064  lebnumlem3  24895  minveclem4a  25363  evthicc  25393  ioorf  25507  deg1ldgn  26031  fta1blem  26109  vieta1lem1  26251  vieta1lem2  26252  vieta1  26253  tanregt0  26481  isosctrlem2  26762  angpieqvd  26774  chordthmlem2  26776  dcubic2  26787  dquartlem1  26794  dquart  26796  asinlem  26811  atandmcj  26852  2efiatan  26861  tanatan  26862  dvatan  26878  dmgmn0  26969  dmgmdivn0  26971  lgamgulmlem2  26973  gamne0  26989  nosep1o  27626  noetasuplem4  27681  footexALT  28698  footexlem1  28699  footexlem2  28700  ttgcontlem1  28865  wlkn0  29601  nrt2irr  30452  fsuppcurry1  32698  fsuppcurry2  32699  bcm1n  32768  mxidlirred  33436  dfufd2  33514  ply1dg1rt  33541  irngnminplynz  33695  minplym1p  33696  minplynzm1p  33697  algextdeglem4  33703  constrrtll  33714  constrrtlc1  33715  constrrtcclem  33717  constrfin  33729  constrelextdg2  33730  cos9thpiminplylem2  33766  zarclssn  33856  sibfof  34324  finxpreclem2  37371  poimirlem9  37616  heicant  37642  heiborlem6  37803  lkrlspeqN  39157  cdlemg18d  40668  cdlemg21  40673  dibord  41146  lclkrlem2u  41514  lcfrlem9  41537  mapdindp4  41710  hdmaprnlem3uN  41838  hdmaprnlem9N  41844  fsuppind  42571  binomcxplemnotnn0  44338  dstregt0  45273  stoweidlem31  46022  stoweidlem59  46050  wallispilem4  46059  dirkertrigeqlem2  46090  fourierdlem43  46141  fourierdlem65  46162  catprs  48993  oppfrcl3  49112  lmdran  49653  cmdlan  49654