Theorem eqnetrrd 3000

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 2999	1 ⊢ (𝜑 → 𝐵 ≠ 𝐶)

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

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 2708

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

This theorem is referenced by:  eqnetrrid  3007  3netr3d  3008  cantnflem1c  9608  eqsqrt2d  15331  tanval2  16100  tanval3  16101  tanhlt1  16127  pcadd  16860  efgsres  19713  gsumval3  19882  ablfac  20065  ablsimpgfind  20087  isdrngrd  20743  isdrngrdOLD  20745  lspsneq  21120  lebnumlem3  24930  minveclem4a  25397  evthicc  25426  ioorf  25540  deg1ldgn  26058  fta1blem  26136  vieta1lem1  26276  vieta1lem2  26277  vieta1  26278  tanregt0  26503  isosctrlem2  26783  angpieqvd  26795  chordthmlem2  26797  dcubic2  26808  dquartlem1  26815  dquart  26817  asinlem  26832  atandmcj  26873  2efiatan  26882  tanatan  26883  dvatan  26899  dmgmn0  26989  dmgmdivn0  26991  lgamgulmlem2  26993  gamne0  27009  nosep1o  27645  noetasuplem4  27700  footexALT  28786  footexlem1  28787  footexlem2  28788  ttgcontlem1  28953  wlkn0  29689  nrt2irr  30543  fsuppcurry1  32797  fsuppcurry2  32798  bcm1n  32868  mxidlirred  33532  dfufd2  33610  ply1dg1rt  33640  esplymhp  33712  irngnminplynz  33856  minplym1p  33857  minplynzm1p  33858  algextdeglem4  33864  constrrtll  33875  constrrtlc1  33876  constrrtcclem  33878  constrfin  33890  constrelextdg2  33891  cos9thpiminplylem2  33927  zarclssn  34017  sibfof  34484  finxpreclem2  37706  poimirlem9  37950  heicant  37976  heiborlem6  38137  lkrlspeqN  39617  cdlemg18d  41127  cdlemg21  41132  dibord  41605  lclkrlem2u  41973  lcfrlem9  41996  mapdindp4  42169  hdmaprnlem3uN  42297  hdmaprnlem9N  42303  fsuppind  43023  binomcxplemnotnn0  44783  dstregt0  45715  stoweidlem31  46459  stoweidlem59  46487  wallispilem4  46496  dirkertrigeqlem2  46527  fourierdlem43  46578  fourierdlem65  46599  catprs  49486  oppfrcl3  49605  lmdran  50146  cmdlan  50147