Theorem eqnetrrd 3084

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

Syntax hints:   → wi 4   = wceq 1533   ≠ wne 3016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-ne 3017

This theorem is referenced by:  eqnetrrid  3091  3netr3d  3092  cantnflem1c  9149  eqsqrt2d  14727  tanval2  15485  tanval3  15486  tanhlt1  15512  pcadd  16224  efgsres  18863  gsumval3  19026  ablfac  19209  ablsimpgfind  19231  isdrngrd  19527  lspsneq  19893  lebnumlem3  23566  minveclem4a  24032  evthicc  24059  ioorf  24173  deg1ldgn  24686  fta1blem  24761  vieta1lem1  24898  vieta1lem2  24899  vieta1  24900  tanregt0  25122  isosctrlem2  25396  angpieqvd  25408  chordthmlem2  25410  dcubic2  25421  dquartlem1  25428  dquart  25430  asinlem  25445  atandmcj  25486  2efiatan  25495  tanatan  25496  dvatan  25512  dmgmn0  25602  dmgmdivn0  25604  lgamgulmlem2  25606  gamne0  25622  footexALT  26503  footexlem1  26504  footexlem2  26505  ttgcontlem1  26670  wlkn0  27401  fsuppcurry1  30460  fsuppcurry2  30461  bcm1n  30517  sibfof  31598  nosep1o  33186  noetalem3  33219  finxpreclem2  34670  poimirlem9  34900  heicant  34926  heiborlem6  35093  lkrlspeqN  36306  cdlemg18d  37816  cdlemg21  37821  dibord  38294  lclkrlem2u  38662  lcfrlem9  38685  mapdindp4  38858  hdmaprnlem3uN  38986  hdmaprnlem9N  38992  binomcxplemnotnn0  40686  dstregt0  41545  stoweidlem31  42315  stoweidlem59  42343  wallispilem4  42352  dirkertrigeqlem2  42383  fourierdlem43  42434  fourierdlem65  42455