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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753  df-ne 2933

This theorem is referenced by:  syl5eqner  3007  3netr3d  3008  cantnflem1c  8757  eqsqrt2d  14307  tanval2  15062  tanval3  15063  tanhlt1  15089  pcadd  15795  efgsres  18351  gsumval3  18508  ablfac  18687  isdrngrd  18975  lspsneq  19324  lebnumlem3  22963  minveclem4a  23401  evthicc  23428  ioorf  23541  deg1ldgn  24052  fta1blem  24127  vieta1lem1  24264  vieta1lem2  24265  vieta1  24266  tanregt0  24484  isosctrlem2  24748  angpieqvd  24757  chordthmlem2  24759  dcubic2  24770  dquartlem1  24777  dquart  24779  asinlem  24794  atandmcj  24835  2efiatan  24844  tanatan  24845  dvatan  24861  dmgmn0  24951  dmgmdivn0  24953  lgamgulmlem2  24955  gamne0  24971  footex  25812  ttgcontlem1  25964  wlkn0  26726  bcm1n  29863  sibfof  30711  nosep1o  32138  noetalem3  32171  finxpreclem2  33538  poimirlem9  33731  heicant  33757  heiborlem6  33928  lkrlspeqN  34961  cdlemg18d  36471  cdlemg21  36476  dibord  36950  lclkrlem2u  37318  lcfrlem9  37341  mapdindp4  37514  hdmaprnlem3uN  37645  hdmaprnlem9N  37651  binomcxplemnotnn0  39057  dstregt0  39992  stoweidlem31  40751  stoweidlem59  40779  wallispilem4  40788  dirkertrigeqlem2  40819  fourierdlem43  40870  fourierdlem65  40891