Theorem eqnetrrd 3010

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

Syntax hints:   → wi 4   = wceq 1539   ≠ wne 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780  df-cleq 2728  df-ne 2942

This theorem is referenced by:  eqnetrrid  3017  3netr3d  3018  cantnflem1c  9489  eqsqrt2d  15125  tanval2  15887  tanval3  15888  tanhlt1  15914  pcadd  16635  efgsres  19389  gsumval3  19553  ablfac  19736  ablsimpgfind  19758  isdrngrd  20062  lspsneq  20429  lebnumlem3  24171  minveclem4a  24639  evthicc  24668  ioorf  24782  deg1ldgn  25303  fta1blem  25378  vieta1lem1  25515  vieta1lem2  25516  vieta1  25517  tanregt0  25740  isosctrlem2  26014  angpieqvd  26026  chordthmlem2  26028  dcubic2  26039  dquartlem1  26046  dquart  26048  asinlem  26063  atandmcj  26104  2efiatan  26113  tanatan  26114  dvatan  26130  dmgmn0  26220  dmgmdivn0  26222  lgamgulmlem2  26224  gamne0  26240  footexALT  27124  footexlem1  27125  footexlem2  27126  ttgcontlem1  27297  wlkn0  28033  fsuppcurry1  31105  fsuppcurry2  31106  bcm1n  31161  zarclssn  31868  sibfof  32352  nosep1o  33929  noetasuplem4  33984  finxpreclem2  35605  poimirlem9  35830  heicant  35856  heiborlem6  36018  lkrlspeqN  37227  cdlemg18d  38737  cdlemg21  38742  dibord  39215  lclkrlem2u  39583  lcfrlem9  39606  mapdindp4  39779  hdmaprnlem3uN  39907  hdmaprnlem9N  39913  fsuppind  40316  binomcxplemnotnn0  42012  dstregt0  42868  stoweidlem31  43621  stoweidlem59  43649  wallispilem4  43658  dirkertrigeqlem2  43689  fourierdlem43  43740  fourierdlem65  43761  catprs  46350