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 1541   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  eqnetrrid  3007  3netr3d  3008  cantnflem1c  9596  eqsqrt2d  15292  tanval2  16058  tanval3  16059  tanhlt1  16085  pcadd  16817  efgsres  19667  gsumval3  19836  ablfac  20019  ablsimpgfind  20041  isdrngrd  20699  isdrngrdOLD  20701  lspsneq  21077  lebnumlem3  24918  minveclem4a  25386  evthicc  25416  ioorf  25530  deg1ldgn  26054  fta1blem  26132  vieta1lem1  26274  vieta1lem2  26275  vieta1  26276  tanregt0  26504  isosctrlem2  26785  angpieqvd  26797  chordthmlem2  26799  dcubic2  26810  dquartlem1  26817  dquart  26819  asinlem  26834  atandmcj  26875  2efiatan  26884  tanatan  26885  dvatan  26901  dmgmn0  26992  dmgmdivn0  26994  lgamgulmlem2  26996  gamne0  27012  nosep1o  27649  noetasuplem4  27704  footexALT  28790  footexlem1  28791  footexlem2  28792  ttgcontlem1  28957  wlkn0  29694  nrt2irr  30548  fsuppcurry1  32803  fsuppcurry2  32804  bcm1n  32875  mxidlirred  33553  dfufd2  33631  ply1dg1rt  33661  esplymhp  33726  irngnminplynz  33869  minplym1p  33870  minplynzm1p  33871  algextdeglem4  33877  constrrtll  33888  constrrtlc1  33889  constrrtcclem  33891  constrfin  33903  constrelextdg2  33904  cos9thpiminplylem2  33940  zarclssn  34030  sibfof  34497  finxpreclem2  37595  poimirlem9  37830  heicant  37856  heiborlem6  38017  lkrlspeqN  39431  cdlemg18d  40941  cdlemg21  40946  dibord  41419  lclkrlem2u  41787  lcfrlem9  41810  mapdindp4  41983  hdmaprnlem3uN  42111  hdmaprnlem9N  42117  fsuppind  42833  binomcxplemnotnn0  44597  dstregt0  45530  stoweidlem31  46275  stoweidlem59  46303  wallispilem4  46312  dirkertrigeqlem2  46343  fourierdlem43  46394  fourierdlem65  46415  catprs  49256  oppfrcl3  49375  lmdran  49916  cmdlan  49917