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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  eqnetrrid  3008  3netr3d  3009  cantnflem1c  9602  eqsqrt2d  15325  tanval2  16094  tanval3  16095  tanhlt1  16121  pcadd  16854  efgsres  19707  gsumval3  19876  ablfac  20059  ablsimpgfind  20081  isdrngrd  20737  isdrngrdOLD  20739  lspsneq  21115  lebnumlem3  24943  minveclem4a  25410  evthicc  25439  ioorf  25553  deg1ldgn  26071  fta1blem  26149  vieta1lem1  26290  vieta1lem2  26291  vieta1  26292  tanregt0  26519  isosctrlem2  26799  angpieqvd  26811  chordthmlem2  26813  dcubic2  26824  dquartlem1  26831  dquart  26833  asinlem  26848  atandmcj  26889  2efiatan  26898  tanatan  26899  dvatan  26915  dmgmn0  27006  dmgmdivn0  27008  lgamgulmlem2  27010  gamne0  27026  nosep1o  27662  noetasuplem4  27717  footexALT  28803  footexlem1  28804  footexlem2  28805  ttgcontlem1  28970  wlkn0  29707  nrt2irr  30561  fsuppcurry1  32815  fsuppcurry2  32816  bcm1n  32886  mxidlirred  33550  dfufd2  33628  ply1dg1rt  33658  esplymhp  33730  irngnminplynz  33875  minplym1p  33876  minplynzm1p  33877  algextdeglem4  33883  constrrtll  33894  constrrtlc1  33895  constrrtcclem  33897  constrfin  33909  constrelextdg2  33910  cos9thpiminplylem2  33946  zarclssn  34036  sibfof  34503  finxpreclem2  37723  poimirlem9  37967  heicant  37993  heiborlem6  38154  lkrlspeqN  39634  cdlemg18d  41144  cdlemg21  41149  dibord  41622  lclkrlem2u  41990  lcfrlem9  42013  mapdindp4  42186  hdmaprnlem3uN  42314  hdmaprnlem9N  42320  fsuppind  43040  binomcxplemnotnn0  44804  dstregt0  45736  stoweidlem31  46480  stoweidlem59  46508  wallispilem4  46517  dirkertrigeqlem2  46548  fourierdlem43  46599  fourierdlem65  46620  catprs  49501  oppfrcl3  49620  lmdran  50161  cmdlan  50162