Theorem eqnetrrd 3001

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 2742	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqnetrrd.2	. 2 ⊢ (𝜑 → 𝐴 ≠ 𝐶)
4	2, 3	eqnetrd 3000	1 ⊢ (𝜑 → 𝐵 ≠ 𝐶)

Syntax hints:   → wi 4   = wceq 1540   ≠ wne 2933

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 2708

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

This theorem is referenced by:  eqnetrrid  3008  3netr3d  3009  cantnflem1c  9706  eqsqrt2d  15392  tanval2  16156  tanval3  16157  tanhlt1  16183  pcadd  16914  efgsres  19724  gsumval3  19893  ablfac  20076  ablsimpgfind  20098  isdrngrd  20731  isdrngrdOLD  20733  lspsneq  21088  lebnumlem3  24918  minveclem4a  25387  evthicc  25417  ioorf  25531  deg1ldgn  26055  fta1blem  26133  vieta1lem1  26275  vieta1lem2  26276  vieta1  26277  tanregt0  26505  isosctrlem2  26786  angpieqvd  26798  chordthmlem2  26800  dcubic2  26811  dquartlem1  26818  dquart  26820  asinlem  26835  atandmcj  26876  2efiatan  26885  tanatan  26886  dvatan  26902  dmgmn0  26993  dmgmdivn0  26995  lgamgulmlem2  26997  gamne0  27013  nosep1o  27650  noetasuplem4  27705  footexALT  28702  footexlem1  28703  footexlem2  28704  ttgcontlem1  28869  wlkn0  29606  nrt2irr  30459  fsuppcurry1  32707  fsuppcurry2  32708  bcm1n  32777  mxidlirred  33492  dfufd2  33570  ply1dg1rt  33597  irngnminplynz  33751  minplym1p  33752  minplynzm1p  33753  algextdeglem4  33759  constrrtll  33770  constrrtlc1  33771  constrrtcclem  33773  constrfin  33785  constrelextdg2  33786  cos9thpiminplylem2  33822  zarclssn  33909  sibfof  34377  finxpreclem2  37413  poimirlem9  37658  heicant  37684  heiborlem6  37845  lkrlspeqN  39194  cdlemg18d  40705  cdlemg21  40710  dibord  41183  lclkrlem2u  41551  lcfrlem9  41574  mapdindp4  41747  hdmaprnlem3uN  41875  hdmaprnlem9N  41881  fsuppind  42580  binomcxplemnotnn0  44347  dstregt0  45277  stoweidlem31  46027  stoweidlem59  46055  wallispilem4  46064  dirkertrigeqlem2  46095  fourierdlem43  46146  fourierdlem65  46167  catprs  48953  oppfrcl3  49045